Skip to content

adds extra indentation on each rewrap (Rocq / .v files only) #425

Description

@RalfJung

There is an odd interaction between Rewrap and VsRocq (https://github.com/rocq-prover/vsrocq):

When I type a comment like this

(** The lemma statement is carefully chosen: we will use this lemma in cases
where [e] is known, so [to_val e] will simplify. We will [eapply] the lemma,
making [v] an evar, which can then be trivially instantiated after
simplification. If we had use [of_val v = e] as the premise, no simplification
would have been possible. *)

and then rewrap 3 times, the result is:

(** The lemma statement is carefully chosen: we will use this lemma in cases
      where [e] is known, so [to_val e] will simplify. We will [eapply] the
      lemma, making [v] an evar, which can then be trivially instantiated after
      simplification. If we had use [of_val v = e] as the premise, no
      simplification would have been possible. *)

The indentation increases by 2 spaces every time I rewrap. Rewrapping should be idempotent (wrapping twice should do the same as wrapping once), so something seems off here. However, strangely I only see this happen in .v files (the extension used by Rocq), not with other file types.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions