Skip to content

Commit

Permalink
Fix #757 indentation of "\in"
Browse files Browse the repository at this point in the history
The lexer now glues a "\" to an immediately following word if it is
itself preceded by a space.

Note that for really good indentation you should try to add something
like this to your configuration:

(setq coq-smie-user-tokens '(("\\in" . "=")))

to tell the indentation grammar that \in has the same precedence as
"=".
  • Loading branch information
Matafou committed Sep 11, 2024
1 parent a36eb9b commit 8e276e6
Showing 1 changed file with 19 additions and 0 deletions.
19 changes: 19 additions & 0 deletions ci/test-indent/test_backslash_ops.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
Require Import mathcomp.ssreflect.ssrbool.

Definition xx := nat.
Module foo.
(* from PG issue #757 *)
Lemma test:
forall a : nat,
a \in [::] -> (* "\in" should be detected as one token *)
False.
Proof.
Abort.

Lemma test2:
forall a : nat,
a \in (* "\in" should be detected as one token *)
[::] ->
False.
End foo.

0 comments on commit 8e276e6

Please sign in to comment.