New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Error after comment is not marked correctly #241

Closed

corwin-of-amber opened this issue Jun 4, 2021 · 0 comments

Member

corwin-of-amber commented Jun 4, 2021

E.g.

  Lemma aux2 a0 b0 a b: (forall z, (z | a0) /\ (z | b0) <-> (z | a) /\ (z | b)) ->
                        a < b ->
                        forall z, (z | a0) /\ (z | b0) <-> (z | a) /\ (z | b - a).
  Proof. (* analogous *)
    error here.

Trying to step through to the error sentence marks it red for a fraction of a second but then immediately clears the mark.

corwin-of-amber added a commit that referenced this issue


          [bugfix] Handling of error markers and comments.

f88555a

Closes #241.

corwin-of-amber closed this as completed in

7b0fe22

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