From 8e276e640b261aac90d8995793e3d5b0795ea642 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 10 Sep 2024 10:23:17 +0200 Subject: [PATCH] Fix #757 indentation of "\in" 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 "=". --- ci/test-indent/test_backslash_ops.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 ci/test-indent/test_backslash_ops.v 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. +