diff --git a/ci/test-indent/test_backslash_ops.v b/ci/test-indent/test_backslash_ops.v new file mode 100644 index 000000000..b350f2fb0 --- /dev/null +++ b/ci/test-indent/test_backslash_ops.v @@ -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. +