From 7e51652aff171d159fb3da132dbb9b8f0a0ae560 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Mon, 3 May 2021 15:56:55 +0200
Subject: [PATCH 1/4] Fix #574 indent of ltac "letins" pattern.

---
 coq/coq-smie.el   | 9 ++++++++-
 coq/coq-syntax.el | 9 +++++++++
 coq/ex/indent.v   | 5 +++++
 3 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 2c3b5772c..88e3375bd 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -552,6 +552,10 @@ The point should be at the beginning of the command name."
      )))
 
 
+(defun coq-is-at-def ()
+  ;; This is very approximate and should be used with care
+  (let ((case-fold-search nil)) (looking-at coq-command-defn-regexp)))
+
 
 ;; ":= with module" is really to declare some sub-information ":=
 ;; with" is for mutual definitions where both sides are of the same
@@ -584,7 +588,10 @@ The point should be at the beginning of the command name."
      ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind
      ((or (eq ?\{ (char-before))) ":= record")
      ((equal (point) cmdstrt)
-      (if (looking-at "Equations") ":="
+      (if (or (looking-at "Equations") ;; note: "[[]" is the regexp for a single "["  
+              (not (coq-is-at-def))
+              )
+          ":="
         ":= def")) ; := outside of any parenthesis
      (t ":=")
      ))) ; a parenthesis stopped the search
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index b8571d24d..afcbd3166 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1381,6 +1381,15 @@ different."
   (concat "\\(" (mapconcat #'identity coq-keywords-defn "\\|")
           "\\)\\s-+\\(" coq-id "\\)"))
 
+;; Any command can be prefixed with Local, Global of #[anyhting,anything,...]
+(defconst coq-command-prefix-regexp "\\(Local\\s-\\|Global\\s-\\|#[[][^]]*[]]\\)")
+;; FIXME: incomplete
+
+(defun coq-add-command-prefix (reg) (concat "\\(" coq-command-prefix-regexp "\\)?" (mapconcat #'identity coq-keywords-defn "\\|")))
+
+(defconst coq-command-decl-regexp (coq-add-command-prefix coq-keywords-decl))
+(defconst coq-command-defn-regexp (coq-add-command-prefix coq-keywords-defn))
+
 ;; must match:
 ;; "with f x y :" (followed by = or not)
 ;; "with f x y (z:" (not followed by =)
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 72a3c2013..2a0d5e478 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -340,6 +340,11 @@ Module X.
         | _ => fail
         end.
 
+        match goal with
+        | ?g := _:rec |- ?a /\ ?b => split
+              | _ => fail
+        end.
+
         Fail
           lazymatch goal with
             _:rec |- ?a /\ ?b => split

From e07f5371000f28094278c02b0695aebd8e9ccb5b Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Sat, 8 May 2021 17:58:20 +0200
Subject: [PATCH 2/4] New smie grammar + indentation rules + tests.

Main design choice for this new version: the first word of a command
is now a token "Com start". Together with the "." token for ending a
command this makes the parsing much more "local".

Users may experience a few changes in the indentation. A few special
cases where the old indentation would reduce shifting to the right
have been removed.

Non regression testing have been added.

See comments in coq-smie.el at coq-smie-grammar for more details.
---
 CHANGES                                      |  10 +
 ci/test-indent/.gitignore                    |   1 +
 ci/test-indent/coq-test-indent.el            |  96 +++
 ci/test-indent/coq-test-indent.sh            |  37 ++
 ci/test-indent/indent-commands-boxed.v       | 268 ++++++++
 ci/test-indent/indent-commands.v             | 265 ++++++++
 ci/test-indent/indent-inside-command-boxed.v | 104 +++
 ci/test-indent/indent-inside-command.v       |  93 +++
 ci/test-indent/indent-tac-boxed.v            | 164 +++++
 ci/test-indent/indent-tac.v                  | 658 +++++++++++++++++++
 ci/test-indent/indent_equations.v            |  79 +++
 ci/test-indent/indent_monadic.v              |  44 ++
 ci/test-indent/tests.sh                      |   8 +
 coq/coq-indent.el                            |   2 +-
 coq/coq-smie.el                              | 568 ++++++++--------
 coq/coq-syntax.el                            |   2 +-
 coq/ex/indent.v                              |   2 +-
 17 files changed, 2122 insertions(+), 279 deletions(-)
 create mode 100644 ci/test-indent/.gitignore
 create mode 100644 ci/test-indent/coq-test-indent.el
 create mode 100755 ci/test-indent/coq-test-indent.sh
 create mode 100644 ci/test-indent/indent-commands-boxed.v
 create mode 100644 ci/test-indent/indent-commands.v
 create mode 100644 ci/test-indent/indent-inside-command-boxed.v
 create mode 100644 ci/test-indent/indent-inside-command.v
 create mode 100644 ci/test-indent/indent-tac-boxed.v
 create mode 100644 ci/test-indent/indent-tac.v
 create mode 100644 ci/test-indent/indent_equations.v
 create mode 100644 ci/test-indent/indent_monadic.v
 create mode 100755 ci/test-indent/tests.sh

diff --git a/CHANGES b/CHANGES
index 56232b34f..56f3da188 100644
--- a/CHANGES
+++ b/CHANGES
@@ -193,6 +193,16 @@ also https://wiki.ubuntu.com/Releases).
     - 92: Compile before require from current directory failing
       with 8.5
 
+*** indentation code refactored
+
+    A big refactoring of the code for indentation has been done. You
+    may experience a few changes in indentation results. Mostly small
+    shifts to the right.
+
+    Variable `coq-indent-box-style' only affects indentation after
+    quantifiers (used to affect script braces "{").
+
+
 * Changes of Proof General 4.4 from Proof General 4.3
 
 ** ProofGeneral has moved to GitHub!
diff --git a/ci/test-indent/.gitignore b/ci/test-indent/.gitignore
new file mode 100644
index 000000000..8e2384ae5
--- /dev/null
+++ b/ci/test-indent/.gitignore
@@ -0,0 +1 @@
+indented_*
\ No newline at end of file
diff --git a/ci/test-indent/coq-test-indent.el b/ci/test-indent/coq-test-indent.el
new file mode 100644
index 000000000..232043313
--- /dev/null
+++ b/ci/test-indent/coq-test-indent.el
@@ -0,0 +1,96 @@
+;;; Regression testing of indentation.
+
+;;; Initially the file is indented as it is supposed to be. Each line
+;;; is unindented, then indented. If the new indentation differ a
+;;; comment is added to signal it.
+
+;;; WARNING: there are relative path names, so this currently works
+;;; only frowhen the current directory is the one containin this file.
+
+(defun blank-line-p ()
+  (= (current-indentation)
+     (- (line-end-position) (line-beginning-position))))
+
+
+(defun line-fixindent ()
+  (save-excursion 
+    (let ((end (line-end-position)))
+      (re-search-forward "fixindent" end t))))
+
+
+(defun test-indent-line (&optional nocomment)
+  (interactive)
+  (unless (or (blank-line-p) (line-fixindent))
+    (back-to-indentation)
+    (let ((init-col (current-column)))
+      ;; avoid moving comments 
+      (unless (proof-inside-comment (point)) (delete-horizontal-space))
+      (indent-according-to-mode)
+      (let ((res (- (current-column) init-col)))
+        (unless (= 0 res)
+          (save-excursion
+            (end-of-line)
+            (unless nocomment
+              (insert (format " (*<=== %s%d INDENT CHANGED *)"
+                              (if (< res 0) "" "+")
+                              res))))
+          res)
+        0))))
+
+
+(defun remove-previous-comment ()
+  (interactive)
+  (save-excursion
+    (end-of-line)
+    (let* ((com (re-search-backward " (\\*<===" (line-beginning-position) t))
+           (strt (and com (point)))
+           (end (and com (line-end-position))))
+      (when com (delete-region strt end)))))
+
+
+(defun test--indent-region (beg end boxed &optional nocomment)
+  (let ((line-move-visual nil)
+        ;; we store the last line number rather than the position
+        ;; since by inderting things we shift the end pos, but not the
+        ;; end line.
+        (last-line (line-number-at-pos end))
+        (stop nil))
+    (set (make-local-variable 'coq-indent-box-style) boxed)
+    (goto-char beg)
+    (while (and (<= (line-number-at-pos) last-line)
+                (not stop))
+      (remove-previous-comment)
+      (test-indent-line nocomment)
+      (setq stop (/= (forward-line) 0)))))
+
+(defun remove-comments-region (beg end)
+  (interactive "r")
+  (goto-char beg)
+  (let ((line-move-visual nil))
+    (while (< (point) end);; loops because end position changes.
+      (remove-previous-comment)
+      (forward-line))))
+
+
+(defun test-indent-region (beg end &optional boxed nocomment)
+  (interactive "r\nP")
+  (test--indent-region beg end boxed nocomment))
+
+
+(defun test-indent-region-boxed (beg end &optional nocomment)
+  (interactive "r")
+  (test--indent-region beg end t nocomment))
+
+
+(defun test-indent-buffer (&optional nocomment) (interactive)
+       (test--indent-region (point-min) (point-max) nil nocomment))
+
+(defun test-indent-buffer-boxed (&optional nocomment) (interactive)
+       (test--indent-region (point-min) (point-max) t nocomment))
+
+(defun launch-test (orig indented &optional boxed)
+    (load-file "../../generic/proof-site.el")
+    (find-file orig)
+    (write-file indented)
+    (if boxed (test-indent-buffer-boxed t) (test-indent-buffer t))
+    (write-file indented))
diff --git a/ci/test-indent/coq-test-indent.sh b/ci/test-indent/coq-test-indent.sh
new file mode 100755
index 000000000..7204d002d
--- /dev/null
+++ b/ci/test-indent/coq-test-indent.sh
@@ -0,0 +1,37 @@
+
+# This script should be launched from its own directory, so that file
+# coq-test-indent.el is accessible.
+
+GREEN='\033[1;32m'
+RED='\033[1;31m'
+MAGENTA='\033[1;35m'
+NC='\033[0m' # No Color
+
+TESTFILE=$1
+INDENTEDTESTFILE=indented_$1
+
+BOXED="nil" 
+if [[ "$1" == *"boxed.v" ]];
+then
+    BOXED="t"
+fi
+
+echo "cp $TESTFILE $INDENTEDTESTFILE"
+cp $TESTFILE $INDENTEDTESTFILE
+
+emacs -q -batch --eval "(progn (load-file \"coq-test-indent.el\") (launch-test \"$TESTFILE\" \"$INDENTEDTESTFILE\" $BOXED))" 
+
+# echo "grep \"INDENT CHANGED\" $INDENTEDTESTFILE"
+# grep "INDENT CHANGED" $INDENTEDTESTFILE
+echo -n " diff -q $TESTFILE $INDENTEDTESTFILE..."
+diff -q $TESTFILE $INDENTEDTESTFILE > /dev/null
+if [[ $? == 1 ]] ;
+then echo " DIFFERENCES FOUND" 
+     printf "${RED} TEST FAILURE ***${NC}\n"
+     echo "  *** details can be seen with:"
+     echo "  ***  diff --side-by-side --suppress-common-lines $TESTFILE $INDENTEDTESTFILE"
+     echo "  *** or graphically: "
+     echo "  ***  meld $TESTFILE $INDENTEDTESTFILE"
+else echo "NO DIFFERENCE"
+     printf "${GREEN} TEST SUCCESS *** ${NC}\n"
+fi
diff --git a/ci/test-indent/indent-commands-boxed.v b/ci/test-indent/indent-commands-boxed.v
new file mode 100644
index 000000000..f22bb5074
--- /dev/null
+++ b/ci/test-indent/indent-commands-boxed.v
@@ -0,0 +1,268 @@
+
+Require Export Coq.Lists.List.
+
+Module Mod.
+
+  Module Foo.
+    Axiom X:Set.
+    Axiom Y:Set.
+    Axiom Z:Set.
+  End Foo.
+  
+  Section Sec.
+    Axiom X:Set.
+    Axiom Y:Set.
+    Axiom Z:Set.
+  End Sec.
+
+  Definition a1 := 1.
+  Definition A2 := 1.
+  Definition arith1:=
+    1.
+  Definition arith1
+    :=
+    1.
+  Definition
+    arith1
+    :=
+    1.
+
+  Let x := 1.  Let y := 2.
+
+  Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+  
+  
+  Inductive test : nat -> Prop :=
+    C1 : forall n, test n
+  | C2 : forall n, test n
+  | C3 : forall n, test n
+  | C4 : forall n, test n.
+  
+  Inductive testbar' : nat -> Prop :=
+  | Cbar1 : forall n, test n
+  | Cbar2 : forall n, test n
+  | Cbar3 : forall n, test n
+  | Cbar4 : forall n, test n.
+  
+  Inductive test2 : nat -> Prop
+    := | C21 : forall n, test2 n
+  | C22 : forall n, test2 n
+  | C23 : forall n, test2 n
+  | C24 : forall n, test2 n.
+  
+  Inductive test' : nat -> Prop :=
+    C1' : forall n, test' n
+  | C2' : forall n, test' n
+  | C3' : forall n, test' n
+  | C4' : forall n, test' n
+  with
+    test2' : nat -> Prop :=
+    C21' : forall n, test2' n
+  | C22' : forall n, test2' n
+  | C23' : forall n, test2' n
+  | C24' : forall n, test2' n
+  with test3' : nat -> Prop :=
+    C21' : forall n, test2' n
+  | C22' : forall n, test2' n
+  | C23' : forall n, test2' n
+  | C24' : forall n, test2' n
+  with test4' : nat -> Prop :=
+  | C21' : forall n, test2' n
+  | C22' : forall n, test2' n
+  | C23' : forall n, test2' n
+  | C24' : forall n, test2' n.
+  
+  
+  Inductive test3
+    : nat -> Prop
+    := C31 : forall n, test3 n
+  | C32 : forall n, test3 n
+  | C33 : forall n, test3 n .
+  
+  (* Goal parenthesizing. *)
+  Lemma L : True.
+  Proof.
+    idtac.
+    idtac... (* special case of command ender. *)
+    idtac.
+  Qed.
+
+  (* Goal starter *)
+  Definition Foo:True.
+    exact I.
+  Defined.
+
+  (* Bullets. *)
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac. idtac.
+    idtac.
+    {
+      idtac.
+      idtac.
+    }
+    idtac. {
+      idtac.
+      idtac. }
+    { idtac.
+      idtac.
+    }
+    {
+      idtac.
+      idtac.
+    }
+    { idtac. {
+        idtac.
+        idtac.
+      }
+      idtac.
+
+      { idtac . {
+          idtac.
+          idtac.
+        }
+      }
+      idtac.
+    }
+    idtac. { idtac. {
+        idtac.
+        idtac.
+      }
+    }
+    idtac.
+    
+    { idtac    . {
+        idtac.
+        idtac.
+      }
+    }
+    {
+      idtac.
+      idtac.
+      idtac. {
+        idtac.
+        idtac.
+      }
+      idtac.
+    }
+  Qed.
+
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac.
+    { idtac.
+      idtac. }
+    { 
+      idtac.
+      idtac.
+    }
+    { idtac. {
+        idtac.
+        idtac.
+      }
+      idtac.
+    }
+    { idtac. idtac. { idtac.
+                      idtac. }
+      idtac.
+    }
+    { idtac. { idtac. {
+          idtac.
+          idtac.
+        }
+        idtac.
+      }
+    }
+    { idtac. { idtac.
+               {
+                 idtac.
+                 idtac.
+               }
+               idtac.
+               idtac.
+               idtac.
+      }
+      idtac.
+    }
+    {
+      idtac.
+      - idtac.
+        idtac. {
+          idtac.
+          idtac.
+        }
+        idtac.
+    }
+  Qed.
+
+
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac.
+    -
+      idtac.
+      idtac.
+    - idtac.
+      idtac.
+      + idtac.
+        idtac.
+      + idtac.
+        idtac.
+        * idtac.
+    - idtac.
+  Qed.
+
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac.
+    -
+      idtac.
+      idtac.
+      idtac.
+      idtac.
+    - idtac.
+      { idtac.
+        - idtac.
+          idtac.
+        - idtac.
+          idtac.
+      }
+    - idtac. idtac. {
+        idtac.
+        - idtac.
+          idtac.
+        - idtac.
+          idtac.
+      }
+      idtac.
+    - idtac.
+  Qed.
+
+
+  (* goal selectors. *)
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac.
+    2:idtac.
+    3-6:idtac.
+
+    2:{ idtac.
+        idtac. }
+    { 
+      idtac.
+      idtac.
+    }
+    [foo]:{
+      idtac.
+      - idtac.
+        idtac. {
+          idtac.
+          idtac.
+        }
+        idtac.
+    }
+  Qed.
+
+
+
+End Mod.
diff --git a/ci/test-indent/indent-commands.v b/ci/test-indent/indent-commands.v
new file mode 100644
index 000000000..9d1c52cb7
--- /dev/null
+++ b/ci/test-indent/indent-commands.v
@@ -0,0 +1,265 @@
+
+Require Export Coq.Lists.List.
+
+Module Mod.
+
+  Module Foo.
+    Axiom X:Set.
+    Axiom Y:Set.
+    Axiom Z:Set.
+  End Foo.
+  
+  Section Sec.
+    Axiom X:Set.
+    Axiom Y:Set.
+    Axiom Z:Set.
+  End Sec.
+
+  Definition a1 := 1.
+  Definition A2 := 1.
+  Definition arith1:=
+    1.
+  Definition arith1
+    :=
+    1.
+  Definition
+    arith1
+    :=
+    1.
+
+  Let x := 1.  Let y := 2.
+               
+  Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+  
+  
+  Inductive test : nat -> Prop :=
+    C1 : forall n, test n
+  | C2 : forall n, test n
+  | C3 : forall n, test n
+  | C4 : forall n, test n.
+  
+  Inductive testbar' : nat -> Prop :=
+  | Cbar1 : forall n, test n
+  | Cbar2 : forall n, test n
+  | Cbar3 : forall n, test n
+  | Cbar4 : forall n, test n.
+  
+  Inductive test2 : nat -> Prop
+    := | C21 : forall n, test2 n
+  | C22 : forall n, test2 n
+  | C23 : forall n, test2 n
+  | C24 : forall n, test2 n.
+  
+  Inductive test' : nat -> Prop :=
+    C1' : forall n, test' n
+  | C2' : forall n, test' n
+  | C3' : forall n, test' n
+  | C4' : forall n, test' n
+  with
+    test2' : nat -> Prop :=
+    C21' : forall n, test2' n
+  | C22' : forall n, test2' n
+  | C23' : forall n, test2' n
+  | C24' : forall n, test2' n
+  with test3' : nat -> Prop :=
+    C21' : forall n, test2' n
+  | C22' : forall n, test2' n
+  | C23' : forall n, test2' n
+  | C24' : forall n, test2' n
+  with test4' : nat -> Prop :=
+  | C21' : forall n, test2' n
+  | C22' : forall n, test2' n
+  | C23' : forall n, test2' n
+  | C24' : forall n, test2' n.
+  
+  
+  Inductive test3
+    : nat -> Prop
+    := C31 : forall n, test3 n
+  | C32 : forall n, test3 n
+  | C33 : forall n, test3 n .
+  
+  (* Goal parenthesizing. *)
+  Lemma L : True.
+  Proof.
+    idtac.
+    idtac... (* special case of command ender. *)
+    idtac.
+  Qed.
+
+  (* Goal starter *)
+  Definition Foo:True.
+    exact I.
+  Defined.
+
+  (* Bullets. *)
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac. idtac.
+    idtac.
+    {
+      idtac.
+      idtac.
+    }
+    idtac. {
+      idtac.
+      idtac. }
+    { idtac.
+      idtac.
+    }
+    {
+      idtac.
+      idtac.
+    }
+    { idtac. {
+        idtac.
+        idtac.
+      }
+      idtac.
+           
+      { idtac . {
+          idtac.
+          idtac.
+        }
+      }
+      idtac.
+    }
+    idtac. { idtac. {
+        idtac.
+        idtac.
+      }
+    }
+    idtac.
+    
+    { idtac    . {
+        idtac.
+        idtac.
+      }
+    }
+    {
+      idtac.
+      idtac.
+      idtac. {
+        idtac.
+        idtac.
+      }
+      idtac.
+    }
+  Qed.
+
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac.
+    { idtac.
+      idtac. }
+    { 
+      idtac.
+      idtac.
+    }
+    { idtac. {
+        idtac.
+        idtac.
+      }
+      idtac.
+    }
+    { idtac. idtac. { idtac.
+                      idtac. }
+      idtac.
+    }
+    { idtac. { idtac. {
+          idtac.
+          idtac.
+    }} }
+    { idtac. { idtac.
+               {
+                 idtac.
+                 idtac.
+               }
+               idtac.
+               idtac.
+               idtac.
+      }
+      idtac.
+    }
+    {
+      idtac.
+      - idtac.
+        idtac. {
+          idtac.
+          idtac.
+        }
+        idtac.
+    }
+  Qed.
+
+
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac.
+    -
+      idtac.
+      idtac.
+    - idtac.
+      idtac.
+      + idtac.
+        idtac.
+      + idtac.
+        idtac.
+        * idtac.
+    - idtac.
+  Qed.
+
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac.
+    -
+      idtac.
+      idtac.
+      idtac.
+      idtac.
+    - idtac.
+      { idtac.
+        - idtac.
+          idtac.
+        - idtac.
+          idtac.
+      }
+    - idtac. idtac. {
+        idtac.
+        - idtac.
+          idtac.
+        - idtac.
+          idtac.
+      }
+      idtac.
+    - idtac.
+  Qed.
+
+
+  (* goal selectors. *)
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof.
+    idtac.
+    2:idtac.
+    3-6:idtac.
+
+    2:{ idtac.
+        idtac. }
+    { 
+      idtac.
+      idtac.
+    }
+    [foo]:{
+      idtac.
+      - idtac.
+        idtac. {
+          idtac.
+          idtac.
+        }
+        idtac.
+    }
+  Qed.
+
+
+
+End Mod.
diff --git a/ci/test-indent/indent-inside-command-boxed.v b/ci/test-indent/indent-inside-command-boxed.v
new file mode 100644
index 000000000..b5b0e9330
--- /dev/null
+++ b/ci/test-indent/indent-inside-command-boxed.v
@@ -0,0 +1,104 @@
+
+Require Export
+        Coq.Lists.List.
+Require
+  Export
+  Arith.
+
+Module
+  Mod.
+
+  Module
+    Foo.
+    Axiom
+      X
+      :
+      Set.
+    Axiom Y
+      :
+      Set.
+    Axiom Z:
+      Set.
+  End
+    Foo.
+  
+
+  Definition a1 :=
+    1.
+  Definition A2
+    := 1.
+  Definition arith1
+    :=
+    1.
+  Definition
+    arith1
+    :=
+    1.
+
+  Let x := 1.  Let y := 2.
+
+  Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+  
+  
+  Inductive test
+    : nat 
+      -> 
+        Prop :=
+    C1 : forall n,
+           test n
+  | C2 : forall n,
+           test
+             n
+  | C3 :
+    forall
+      n, test n
+  | C4 : forall n, test n.
+  
+  
+  (* Goal parenthesizing. *)
+  Lemma L :
+    True.
+  Proof.
+    idtac.
+    idtac... (* special case of command ender. *)
+    idtac.
+  Qed.
+
+
+  Lemma L4 : forall x:nat,
+               Nat.iter x (A:=nat)
+                        (plus 2) 0 >= x.
+  Proof.
+    idtac.
+  Qed.
+
+  Lemma L3 : forall x:nat,
+               Nat.iter
+                 x 
+                 (A:=nat)
+                 (plus 2)
+                 0 >= x.
+  Proof.
+    idtac.
+  Qed.
+
+  Lemma L1 : forall x:nat, Nat.iter x 
+                                    (A:=nat)
+                                    (plus 2)
+                                    0 >= x.
+  Proof.
+    idtac.
+  Qed.
+
+  Lemma L2 : forall x:nat, Nat.iter
+                             x 
+                             (A:=nat)
+                             (plus 2)
+                             0 >= x.
+  Proof.
+    idtac.
+  Qed.
+
+
+
+End Mod.
diff --git a/ci/test-indent/indent-inside-command.v b/ci/test-indent/indent-inside-command.v
new file mode 100644
index 000000000..5ad50e6ee
--- /dev/null
+++ b/ci/test-indent/indent-inside-command.v
@@ -0,0 +1,93 @@
+
+Require Export
+        Coq.Lists.List.
+Require
+  Export
+  Arith.
+
+Module
+  Mod.
+
+  Module
+    Foo.
+    Axiom
+      X
+      :
+      Set.
+    Axiom Y
+      :
+      Set.
+    Axiom Z:
+      Set.
+  End
+    Foo.
+  
+
+  Definition a1 :=
+    1.
+  Definition A2
+    := 1.
+  Definition arith1
+    :=
+    1.
+  Definition
+    arith1
+    :=
+    1.
+
+  Let x := 1.  Let y := 2.
+
+  Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+  
+  
+  Inductive test
+    : nat 
+      -> 
+        Prop :=
+    C1 : forall n,
+        test n
+  | C2 : forall n,
+      test
+        n
+  | C3 :
+    forall
+      n, test n
+  | C4 : forall n, test n.
+
+  Lemma L4 : forall x:nat,
+      Nat.iter x (A:=nat)
+               (plus 2) 0 >= x.
+  Proof.
+    idtac.
+  Qed.
+
+  Lemma L3 : forall x:nat,
+      Nat.iter
+        x 
+        (A:=nat)
+        (plus 2)
+        0 >= x.
+  Proof.
+    idtac.
+  Qed.
+
+  Lemma L1 : forall x:nat, Nat.iter x 
+                                    (A:=nat)
+                                    (plus 2)
+                                    0 >= x.
+  Proof.
+    idtac.
+  Qed.
+
+  Lemma L2 : forall x:nat, Nat.iter
+                             x 
+                             (A:=nat)
+                             (plus 2)
+                             0 >= x.
+  Proof.
+    idtac.
+  Qed.
+
+
+
+End Mod.
diff --git a/ci/test-indent/indent-tac-boxed.v b/ci/test-indent/indent-tac-boxed.v
new file mode 100644
index 000000000..8c37d910e
--- /dev/null
+++ b/ci/test-indent/indent-tac-boxed.v
@@ -0,0 +1,164 @@
+Module foo.
+  Lemma toto:nat.
+  Proof.
+    {{
+        exact 3.
+    }}
+  Qed.
+
+  Lemma foo: forall n: nat,
+             exists m:nat,
+               m = n + 1.
+  Proof.
+    intros n.
+    destruct n. {
+      exists 1.
+      reflexivity. }
+    exists (S (S n)).
+    simpl.
+    rewrite Nat.add_1_r.
+    reflexivity.
+  Qed.
+
+  Lemma L : forall x:nat,
+              Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    intros x.
+    
+    induction x;simpl;intros...
+    
+    induction x;
+      simpl ;
+      simpl ;
+      simpl ;
+      intros.
+  Qed.
+  
+  Ltac foo:= intros x;
+             induction x;
+             simpl ;
+             intros.
+  
+
+  Lemma L :
+    forall x:nat ,
+      Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    intros x;
+      induction x;
+      simpl ;
+      intros.
+    idtacjqslkjd;[
+        intros x ;
+        induction x ;
+        simpl ;
+        intros].
+  Qed.
+
+
+
+  Lemma L' : forall x:nat ,
+               Nat.iter x (A:=nat) (plus 2) 0 >= x
+  with L'' : forall x:nat ,
+               Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    - induction x;simpl;intros...
+    - induction x;simpl;intros...
+  Qed.
+
+End foo.
+
+Section SET.
+  Definition set (T : Type) := Ensemble T.
+  
+  Require Import Program.
+  
+  
+  Definition eq_n : forall A n (v:Vector.t A n) n',
+                      n=n' ->
+                      Vector.t A n'.
+  Proof.
+    intros A n v n' H.
+    rewrite <- H.
+    assumption.
+  Defined.
+  
+End SET.
+
+Module curlybracesatend.
+
+  
+  Lemma foo2: forall n: nat,
+              exists m:nat,
+                m = n + 1.
+  Proof.
+    intros n.
+    destruct n. {
+      exists 1.
+      reflexivity. }
+    
+    exists (S (S n)).
+    simpl.
+    rewrite Nat.add_1_r.
+    reflexivity.
+  Qed.
+  
+  Lemma foo3: forall n: nat,
+              forall n: nat,
+              forall n: nat,
+              forall n: nat, forall n: nat,
+              exists m:nat,
+                m = n + 1 ->
+                m = n + 1 ->
+                m = n + 1
+                -> m = n + 1
+                -> m = n + 1 ->
+                m = n + 1.
+  Proof.
+    intros n. cut (n = n). {
+      destruct n. {
+        exists 1.
+        reflexivity. } {
+        exists (S (S n)).
+        simpl.
+        rewrite Nat.add_1_r.
+        reflexivity. }
+    }
+    idtac.
+    reflexivity.
+  Qed.
+
+  Lemma foooooooooooooooo3: forall n: nat,
+                            forall n: nat, forall n: nat,
+                              f x ->
+                              g y ->
+                              f x -> forall n: nat,
+                                     forall n: nat,
+                                     forall n: nat,
+                                     exists m:nat,
+                                       m = n + 1 ->
+                                       m = n + 1 ->
+                                       m = n + 1
+                                       -> m = n + 1
+                                       -> m = n + 1 ->
+                                       m = n + 1 -> 
+                                       True.
+  Proof.
+    intros n. cut (n = n).
+    {
+      destruct n. {
+        exists 1.
+        reflexivity. } {
+        exists (S (S n)).
+        simpl.
+        rewrite Nat.add_1_r.
+        reflexivity.
+      }
+    }
+    idtac.
+    reflexivity.
+  Qed.
+
+  
+End curlybracesatend.
+
diff --git a/ci/test-indent/indent-tac.v b/ci/test-indent/indent-tac.v
new file mode 100644
index 000000000..7e474d4cf
--- /dev/null
+++ b/ci/test-indent/indent-tac.v
@@ -0,0 +1,658 @@
+
+Module foo.
+  Lemma toto:nat.
+  Proof.
+    {{
+        exact 3.
+    }}
+  Qed.
+
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    intros x.
+    
+    induction x;simpl;intros...
+
+    induction x;
+      simpl ;
+      simpl ;
+      simpl ;
+      intros.
+
+    Ltac foo:=
+      intros x;
+      induction x;
+      simpl ;
+      simpl ;
+      simpl ;
+      intros.
+
+    
+    induction x
+    ;
+      simpl
+    ;
+      intros
+    ;
+      intros
+    ;
+      intros
+    .
+    
+    
+    idtac
+    ;
+      [
+        induction x
+        ;
+          simpl
+        ;
+          intros
+      ].
+
+    
+    Ltac foo
+      :=
+      intros x
+      ;
+        induction x
+      ;
+        simpl
+      ;
+        intros
+      ;
+        intros
+    .
+    
+
+    idtac
+    ;
+      [
+        induction x
+        ;
+          simpl ;
+        simpl
+      | intros
+      ].
+    
+    Ltac foo :=
+      intros x
+      ;
+        induction x
+      ;
+        simpl
+      ;
+        intros
+      ;
+        intros
+    .
+    
+
+
+
+    induction x ;
+      simpl ;
+      intros.
+
+    induction x
+    ;
+      simpl ;
+      intros.
+
+    induction x ;
+      simpl
+    ;
+      simpl ;
+      intros.
+    
+    
+    intros x
+    ; induction x
+    ; simpl
+    ; intros.
+    
+    idtac;(intros x
+           ; induction x
+           ; simpl
+           ; intros).
+    
+
+    idtac;( induction x;
+            simpl ;
+            intros ).
+    
+    idtac;[ intros x
+            ; induction x
+            ; simpl
+            ; intros].
+
+    idtac
+    ;
+      [
+        induction x;
+        simpl ;
+        intros
+      | simpl
+        ; intros ].
+
+
+    idtac;[ intros x
+            ; induction x
+          | simpl
+            ; intros].
+    
+
+    idtac;[ intros x ;
+            induction x
+          | simpl ;
+            intros
+      ].
+    
+
+    idtac foobar;[ induction x;
+                   simpl ;
+                   intros ].
+
+  Qed.
+
+  Ltac foo:=
+    intros x;
+    induction x;
+    simpl ;
+    intros.
+  
+
+  Lemma L :
+    forall x:nat ,
+      Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    intros x;
+      induction x;
+      simpl ;
+      intros.
+    idtacjqslkjd;[
+        intros x ;
+        induction x ;
+        simpl ;
+        intros].
+  Qed.
+  Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    intros x;
+      [ induction x;
+        [
+          simpl;
+          intros...
+        ]
+      ]
+  Qed.
+
+
+  Lemma L2 : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    idtac.
+    (* "as" tactical *)
+    induction x
+      as
+      [ | x IHx]. 
+    - cbn.
+      apply Nat.le_trans
+        with
+        (n:=0) (* aligning the different closes of a "with". *)
+        (m:=0)
+        (p:=0).
+      + auto with arith.
+      + auto with arith.
+    - simpl.
+      intros.
+      auto with arith.
+  Qed.
+
+  Lemma L' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x
+  with L'' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof with auto with arith.
+    - induction x;simpl;intros...
+    - induction x;simpl;intros...
+  Qed.
+  Lemma L''' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+  Proof using Type *.
+    intros x.
+    induction x;simpl;intros.  
+    admit.
+  Admitted.
+
+  Lemma L'''' : forall x:nat ,  0 <= x.
+  Proof (fun x : nat => Nat.le_0_l x).
+  (* no indentation here since the proof above closes the proof. *)
+  Definition foo:nat := 0.
+End Y.
+
+Function div2 (n : nat) {struct n}: nat :=
+  match n with
+  | 0 => 0
+  | 1 => 0
+  | S (S n') => S (div2 n')
+  end.
+
+
+Module M1.
+  Module M2.
+    Lemma l1: forall n:nat, n = n. 
+      auto.
+    Qed.
+    Lemma l2: forall n:nat, n = n. 
+      auto. Qed.
+    Lemma l3: forall n:nat, n <= n. auto. Qed.
+    (*   Lemma l4: forall n:nat, n <= n. Proof. intro. Qed. *)
+    Lemma l5 : forall n:nat, n <= n.
+    Proof. auto.
+    Qed.
+    Lemma l6: forall n:nat, n = n. 
+      intros.
+      Lemma l7: forall n:nat, n = n.
+        destruct n.
+        {
+          auto.
+        }
+        {
+          destruct n.
+          {
+            auto.
+          }
+          auto.
+        }
+      Qed.
+      {
+        destruct n.
+        {
+          auto. }
+        { auto.
+        }
+      }
+    Qed.
+  End M2.
+End M1.
+
+Module GoalSelectors.
+  Theorem lt_n_S : (True \/ True \/ True \/ True \/ True ) -> True.
+  Proof.
+    refine (or_ind ?[aa] (or_ind ?[bb] (or_ind ?[cc] (or_ind ?[dd] ?[ee])))).
+    [aa]:{ auto. }
+    2:{  auto. }
+    [ee]:auto.
+    {  auto.}
+  Qed.
+  (* Same without space between "." and "}". *)
+  Theorem lt_n_S2 : (True \/ True \/ True \/ True \/ True ) -> True.
+  Proof.
+    refine (or_ind ?[aa] (or_ind ?[bb] (or_ind ?[cc] (or_ind ?[dd] ?[ee])))).
+    [aa]:{ auto.}
+    2:{  auto.}
+    [ee]:auto.
+    {  auto.}
+  Qed.
+
+
+End GoalSelectors.
+
+Module M1'.
+  Module M2'.
+    Lemma l6: forall n:nat, n = n.
+    Proof.
+      intros.
+      Lemma l7: forall n:nat, n = n.
+      Proof.
+        destruct n. intros.
+        {
+          auto.
+        }
+        { 
+          destruct n. 
+          idtac a
+          ;
+            [
+              auto;
+              auto
+            |
+              auto;
+              auto.
+            ].
+        }
+        auto.
+        } 
+      Qed.
+      {destruct n.
+       {
+         auto. }
+       {auto. }
+      }
+    Qed.
+  End M2'.
+End M1'.
+
+(* TODO: add multichar bullets once coq 8.5 is out *)
+Module M4'.
+  Module M2'.
+    Lemma l6: forall n:nat, n = n. 
+    Proof.
+      intros.
+      Lemma l7: forall n:nat, n = n. 
+      Proof.
+        destruct n.
+        - auto.
+        - destruct n.
+          + idtac;[
+                auto
+              ].
+          + destruct n.
+            * auto.
+            * auto.
+      Qed.
+      {destruct n.
+       - auto.
+       - auto. 
+      }
+    Qed.
+  End M2'.
+End M4'.
+
+
+Module M1''.
+  Module M2''.
+    Lemma l7: forall n:nat, n = n. 
+      destruct n.
+      { auto. }
+      { destruct n.
+        { idtac; [ auto ]. }
+        auto. } 
+    Qed.
+  End M2''.
+End M1''.
+
+
+Record rec:Set := {
+    fld1:nat;
+    fld2:nat;
+    fld3:bool
+  }.
+
+Class cla {X:Set}:Set := {
+    cfld1:nat;
+    cld2:nat;
+    cld3:bool
+  }.
+
+
+
+Module X.
+  Lemma l:
+    forall r:rec,
+    exists r':rec,
+      r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1).
+  Proof.
+    idtac.
+    idtac.
+    idtac.
+    intros r. {
+      exists
+        {|
+          fld1:=r.(fld2);
+          fld2:=r.(fld1);
+          fld3:=false
+        |}.
+      split.
+      {auto. }
+      {auto. }
+    }
+    auto.
+    auto.
+  Qed.
+  
+  (* Issue #574 *)
+  Goal let x := 1 in True.
+  Proof.
+    intro.
+    match goal with
+    | y := _ : unit |- _ => idtac "unit"
+    | y := _ : nat |- _ => idtac "nat"
+    end.
+  Qed.
+
+  Lemma l2 :
+    forall r:rec,
+    exists r':rec,
+      r.(fld1)
+      = r'.(fld2)
+      /\ r.(fld2)
+         = r'.(fld1).
+  Proof.
+    intros r.
+    {{
+        idtac;
+          exists
+            {|
+              fld1:=r.(fld2);
+              fld2:=r.(fld1);
+              fld3:=false
+            |}.
+        (* ltac *)
+        match goal with
+          _:rec |- ?a /\ ?b => split
+        | _ => fail
+        end.
+
+        match goal with
+        | ?g := _:rec |- ?a /\ ?b => split
+        | _ => fail
+        end.
+
+        Fail
+          lazymatch goal with
+            _:rec |- ?a /\ ?b => split
+          | _ => fail
+          end.
+
+        Fail
+          multimatch goal with
+            _:rec |- ?a /\ ?b => split
+          | _ => fail
+          end.
+
+        { simpl. auto. }
+        { simpl. auto. }}}
+
+    - split.
+      match
+        goal
+      with
+        X => foo
+      end.
+    - split.
+      match goal with
+        X |- _ => foo
+      | H: X := Y |- _ => foo
+      end.
+    - split.
+      match H with
+        ?a = ?b |- _ => foo
+      | ?a < ?b |- _ => foo
+      end.
+    - split.
+      let x := f y in
+      let foo := idtac x in
+      idtac foo.
+  Qed.
+End X.
+
+Require Import Morphisms.
+Generalizable All Variables.
+Local Open Scope signature_scope.
+Require Import RelationClasses.
+
+Module TC.
+  Instance: (@RewriteRelation nat) impl.
+  (* No goal created *)
+  Definition XX := 0.
+  
+  
+  Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R.
+  (* One goal created. Then the user MUST put "Proof." to help indentation *)
+  Proof.
+    firstorder.
+  Qed.
+  
+  
+  Program Fixpoint f (x:nat) {struct x} : nat :=
+    match x with
+    | 0 => 0
+    | S y => S (f y)
+    end.
+  
+  Program Instance all_iff_morphism {A : Type} :
+    Proper (pointwise_relation A iff ==> iff) (@all A).
+  
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intro.
+    intros y H.    
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+  
+End TC.
+
+Require Import Sets.Ensembles.
+Require Import Bool.Bvector.
+
+Section SET.
+  Definition set (T : Type) := Ensemble T.
+  
+  Require Import Program.
+  
+  
+  Definition eq_n : forall A n (v:Vector.t A n) n', n=n' -> Vector.t A n'.
+  Proof.
+    intros A n v n' H.
+    rewrite <- H.
+    assumption.
+  Defined.
+  
+  Fixpoint setVecProd (T : Type) (n : nat) (v1:Vector.t (set T) n) {struct v1}:
+    (Vector.t T n) ->  Prop :=
+    match v1 with
+      Vector.nil _ =>
+        fun v2 =>
+          match v2 with 
+            Vector.nil _ => True
+          | _ => False
+          end
+    | (Vector.cons _ x n' v1') =>
+        fun v2 =>
+          (* indentation of dependen "match" clause. *)
+          match v2
+                as
+                X
+                in
+                Vector.t _ n''
+                return
+                (Vector.t T (pred n'') -> Prop) -> Prop
+          with 
+          | Vector.nil _ => fun _ => False 
+          | (Vector.cons _ y n'' v2') => fun v2'' => (x y) /\ (v2'' v2')
+          end (setVecProd T n' v1')
+    end.
+  
+End SET.
+
+Module curlybracesatend.
+
+  Lemma foo: forall n: nat,
+    exists m:nat,
+      m = n + 1.
+  Proof.
+    intros n.
+    destruct n. {
+      exists 1.
+      reflexivity. }
+    exists (S (S n)).
+    simpl.
+    rewrite Nat.add_1_r.
+    reflexivity.
+  Qed.
+  
+  Lemma foo2: forall n: nat,
+    exists m:nat,
+      m = n + 1.
+  Proof.
+    intros n.
+    destruct n. {
+      exists 1.
+      reflexivity. }
+    
+    exists (S (S n)).
+    simpl.
+    rewrite Nat.add_1_r.
+    reflexivity.
+  Qed.
+  
+  Lemma foo3:
+    forall n: nat,
+    forall n: nat,
+    forall n: nat,
+    forall n: nat,
+    forall n: nat,
+    exists m:nat,
+      m = n + 1 ->
+      m = n + 1 ->
+      m = n + 1
+      -> m = n + 1
+      -> m = n + 1 ->
+      m = n + 1.
+  Proof.
+    intros n. cut (n = n). {
+      destruct n. {
+        exists 1.
+        reflexivity. } {
+        exists (S (S n)).
+        simpl.
+        rewrite Nat.add_1_r.
+        reflexivity. }
+    }
+    idtac.
+    reflexivity.
+  Qed.
+
+  Lemma foooooooooooooooo3: forall n: nat,
+    forall n: nat, forall n: nat,
+      f x ->
+      g y ->
+      f x -> forall n: nat,
+        forall n: nat,
+        forall n: nat,
+        exists m:nat,
+          m = n + 1 ->
+          m = n + 1 ->
+          m = n + 1
+          -> m = n + 1
+          -> m = n + 1 ->
+          m = n + 1 -> 
+          True.
+  Proof.
+    intros n. cut (n = n).
+    {
+      destruct n. {
+        exists 1.
+        reflexivity. } {
+        exists (S (S n)).
+        simpl.
+        rewrite Nat.add_1_r.
+        reflexivity.
+      }
+    }
+    idtac.
+    reflexivity.
+  Qed.
+
+  
+End curlybracesatend.
+
diff --git a/ci/test-indent/indent_equations.v b/ci/test-indent/indent_equations.v
new file mode 100644
index 000000000..3e200b5f2
--- /dev/null
+++ b/ci/test-indent/indent_equations.v
@@ -0,0 +1,79 @@
+(* Needs Equations plugin to work. *)
+
+From Coq Require Import Arith Omega Program.
+From Equations Require Import Equations.
+Require Import Bvector.
+
+
+Module Equations.
+  Equations neg (b : bool) : bool :=
+    neg true := false ;
+    neg false := true.
+
+  Lemma neg_inv : forall b, neg (neg b) = b.
+  Proof.
+    intros b.
+    funelim (neg b); now simp neg.
+  Defined.
+
+
+  Inductive list {A} : Type := nil : list | cons : A -> list -> list.
+
+  Arguments list : clear implicits.
+  Notation "x :: l" := (cons x l). 
+
+  Equations tail {A} (l : list A) : list A :=
+  | nil := nil ;
+  | (cons a v) := v.
+
+  Equations tail' {A} (l : list A) : list A :=
+  | nil :=
+      nil ;
+  | (cons a v)
+      := v.
+
+  (* The cases inside { } are recognized as record fields, which from
+     an indentation perspective is OK *)
+  Equations filter {A} (l : list A) (p : A -> bool) : list A :=
+    filter nil p := nil; 
+    filter (cons a l) p with p a => { 
+      | true := a :: filter l p ;
+      | false := filter l p
+      }.
+
+  Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
+    filter' (cons a l) p with p a =>
+      { 
+      | true := a :: filter' l p ;
+      | false := filter' l p
+      };
+    filter' nil p := nil.
+
+  Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
+    filter' (cons a l) p with p a =>
+      { 
+        true := a :: filter' l p ;
+        false := filter' l p
+      };
+    filter' nil p := nil.
+
+  Equations filter'' {A} (l : list A) (p : A -> bool) : list A :=
+    filter'' (cons a l) p with p a =>
+      { | true := a :: filter'' l p ;
+      | false := filter'' l p };
+    filter'' nil p := nil.
+
+  Equations unzip {A B} (l : list (A * B)) : list A * list B :=
+    unzip nil := (nil, nil) ;
+    unzip (cons p l) with unzip l => {
+        unzip (cons (pair a b) l) (pair la lb) := (a :: la, b :: lb) }.
+
+
+  Equations equal (n m : nat) : { n = m } + { n <> m } :=
+    equal O O := left eq_refl ;
+    equal (S n) (S m) with equal n m :=
+      { equal (S n) (S ?(n)) (left eq_refl) := left eq_refl ;
+        equal (S n) (S m) (right p) := right _ } ;
+    equal x y := right _.
+  
+End Equations.
diff --git a/ci/test-indent/indent_monadic.v b/ci/test-indent/indent_monadic.v
new file mode 100644
index 000000000..1cc6e8c1a
--- /dev/null
+++ b/ci/test-indent/indent_monadic.v
@@ -0,0 +1,44 @@
+(* Needs ext-lib library to compile. *)
+
+Require Import Coq.ZArith.ZArith_base Coq.Strings.Ascii Coq.Strings.String.
+Require Import ExtLib.Data.Monads.StateMonad ExtLib.Structures.Monads.
+Import StringSyntax.
+Open Scope string_scope.
+Section StateGame.
+  
+  Check Ascii.Space.
+
+  Import MonadNotation.
+  Local Open Scope Z_scope.
+  Local Open Scope char_scope.
+  Local Open Scope monad_scope.
+
+  Definition GameValue : Type := Z.
+  Definition GameState : Type := (prod bool Z).
+
+  Variable m : Type -> Type.
+  Context {Monad_m: Monad m}.
+  Context {State_m: MonadState GameState m}.
+
+  Print Grammar constr.
+
+  Fixpoint playGame (s: string) m' {struct s}: m GameValue :=
+    match s with
+    | EmptyString =>
+        v <- (if true then m' else get) ;;
+        let '(on, score) := v in ret score
+    | String x xs =>
+        v <- get ;;
+        let '(on, score) := v in
+        match x, on with
+        | "a"%char, true =>  put (on, score + 1)
+        | "b"%char, true => put (on, score - 1)
+        | "c"%char, _ =>   put (negb on, score)
+        |  _, _  =>    put (on, score)
+        end ;;
+        playGame xs m'
+    end.
+
+  Definition startState: GameState := (false, 0).
+
+End StateGame.
diff --git a/ci/test-indent/tests.sh b/ci/test-indent/tests.sh
new file mode 100755
index 000000000..9dcd5c095
--- /dev/null
+++ b/ci/test-indent/tests.sh
@@ -0,0 +1,8 @@
+
+
+
+
+for i in $(find . -name "*.v" -exec basename '{}' \; | grep -v "indented_") ; do
+    echo -n "Testing $i..."
+    ./coq-test-indent.sh $i 2>&1 | tee .$i.log | grep "\*\*\*"
+done
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 3a531e571..715c1e280 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -78,7 +78,7 @@ No context checking.")
 (defconst coq-bullet-prefix-regexp-backward
   (concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp-backward "\\)\\(?:\\.\\s-+\\)"
           "\\(?:\\(?:" coq-goal-selector-regexp "\\)?"
-          "{\\|}\\|-\\|+\\|\\*\\)*\\)"))
+          "{\\|}\\|-\\|+\\|\\*\\s-\\)*\\)"))
 
 ;; matches regular command end (. and ... followed by a space or "}" or buffer end)
 ;; ". " and "... " are command endings, ".. " is not, same as in
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 88e3375bd..b3357d065 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -162,7 +162,8 @@ attention to case differences."
          (cmdstrt (save-excursion (coq-find-real-start)))
          (enclosing (coq-is-inside-enclosing cmdstrt)))
     (cond
-     ((string-equal enclosing "{|") nil)
+     ((string-equal enclosing "{|") nil) ;; only records
+     ((and enclosing (string-match "{" enclosing)) nil) ;; more agressive: record-like notations
      (t (save-excursion
           (goto-char cmdstrt)
           (let ((case-fold-search nil))
@@ -486,13 +487,14 @@ The point should be at the beginning of the command name."
        (t (save-excursion (coq-smie-backward-token))))) ;; recursive call
      ((or (string-match coq-bullet-regexp-nospace tok)
 	  (member tok '("=>" ":=" "::=" "exists" "in" "as" "∀" "∃" "→" "∨" "∧" ";"
-			"," ":" "eval")))
+			"," ":" "eval" "return")))
       ;; The important lexer for indentation's performance is the backward
       ;; lexer, so for the forward lexer we delegate to the backward one when
       ;; we can.
       (save-excursion (coq-smie-backward-token)))
 
-     ((member tok '("lazymatch" "lazy_match" "multimatch" "multi_match")) "match")
+     ;; match needs to be catpured now to avoid being catpured by "Com start"
+     ((member tok '("match" "lazymatch" "lazy_match" "multimatch" "multi_match")) "match")
 
      ;; detect "with signature", otherwies use coq-smie-backward-token
      ((equal tok "with")
@@ -547,6 +549,16 @@ The point should be at the beginning of the command name."
      ((coq-dot-friend-p tok) ".")
      ;; Try to rely on backward-token for non empty tokens: bugs (hangs)
      ;; ((not (zerop (length tok))) (save-excursion (coq-smie-backward-token)))
+
+     ;; Com start is a token for the first word of a command (provided it is a word)
+     ((save-excursion
+        (and (smie-default-backward-token) 
+             (coq-is-at-command-real-start)
+             (> (length tok) 0)
+             (or (string= "Lu" (get-char-code-property (aref tok 0) 'general-category))
+                 (string= "Ll" (get-char-code-property (aref tok 0) 'general-category)))))
+      "Com start")
+
      ;; return it.
      (tok)
      )))
@@ -556,6 +568,11 @@ The point should be at the beginning of the command name."
   ;; This is very approximate and should be used with care
   (let ((case-fold-search nil)) (looking-at coq-command-defn-regexp)))
 
+(defun coq-is-at-def-or-decl ()
+  ;; This is very approximate and should be used with care
+  (let ((case-fold-search nil))
+    (or (looking-at coq-command-defn-regexp) (looking-at coq-command-decl-regexp))))
+
 
 ;; ":= with module" is really to declare some sub-information ":=
 ;; with" is for mutual definitions where both sides are of the same
@@ -588,13 +605,11 @@ The point should be at the beginning of the command name."
      ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind
      ((or (eq ?\{ (char-before))) ":= record")
      ((equal (point) cmdstrt)
-      (if (or (looking-at "Equations") ;; note: "[[]" is the regexp for a single "["  
-              (not (coq-is-at-def))
-              )
-          ":="
-        ":= def")) ; := outside of any parenthesis
-     (t ":=")
-     ))) ; a parenthesis stopped the search
+      ;; we reached the command start: either we were in an Equation,
+      ;; or the ":=" was inpatter of an Ltac match (pattern the form
+      ;; "| H: T := t |- _"). Toherwise we are probably in a Definition.
+      (if (or (looking-at "Equations\\|match\\|let")) ":=" ":= def"))
+     (t ":="))))
 
 
 (defun coq-smie-semicolon-deambiguate ()
@@ -631,6 +646,8 @@ The point should be at the beginning of the command name."
     (cond
      ;; Distinguish between "," from quantification and other uses of
      ;; "," (tuples, tactic arguments)
+     ;; we cannot distinguish between tuples and tac args, because of:
+     ;; an term (f x , v) and a tactic expecting a tuple (tac x , v)
      ((equal tok ",")
       (save-excursion
 	(let ((backtok (coq-smie-search-token-backward
@@ -702,7 +719,8 @@ The point should be at the beginning of the command name."
 	;(coq-find-real-start)
 	(coq-smie-module-deambiguate)))
 
-     ((member tok '("lazy_?match" "multi_?match")) "match")
+     ;; match needs to be catpured now to avoid being catpured by "Com start"
+     ((member tok '("match" "lazy_match" "lazymatch" "multi_match" "multimatch")) "match")
 
      ((equal tok "tryif") "if")
 
@@ -737,7 +755,7 @@ The point should be at the beginning of the command name."
      ;;         (let ((nxttok (coq-smie-backward-token))) ;; recursive call
      ;;           (coq-is-cmdend-token nxttok))))
      ;;  (forward-char -1)
-     ;;  (if (looking-at "{") "{ subproof" "} subproof"))
+     ;;  (if (looking-at "{") "{ subproof" "} subproof")))
 
      ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac2?\\|uconstr\\)"
                                          (- (point) 7)))
@@ -817,6 +835,17 @@ The point should be at the beginning of the command name."
 	   ((member prev-interesting '("Morphism" "Relation")) "as morphism")
 	   (t tok)))))
 
+     ((equal tok "return")
+      (save-excursion
+	(let ((prev-interesting
+	       (coq-smie-search-token-backward
+		'("match" "lazymatch" "multimatch" "lazy_match" "multi_match" "Morphism" "Relation" "." ". proofstart")
+		nil
+		'((("match" "lazy_match" "multi_match" "let") . "with") ("with" . "signature")))))
+	  (cond
+	   ((member prev-interesting '("match" "lazymatch" "multimatch" "lazy_match" "mult_match")) "return match")
+	   (t tok)))))
+
      ((equal tok "by")
       (let ((p (point)))
 	(if (and (equal (smie-default-backward-token) "proved")
@@ -883,11 +912,26 @@ The point should be at the beginning of the command name."
       (let ((newtok (coq-smie-backward-token))) ; recursive call
 	(concat newtok "." tok)))
 
-     ;; easier to return directly than calling coq-smie-backward-token
      ((member tok '("lazymatch" "lazy_match" "multimatch" "multi_match")) "match")
 
-
      ((coq-dot-friend-p tok) ".")
+
+     ;; Default fallback for words at command start position: We use a
+     ;; generic "Com start" token, so that everything in the command
+     ;; is considered a child of this token. This makes indentation
+     ;; never look above the current command start (unless indenting
+     ;; the first line of the command. For now we only apply this to
+     ;; things starting with a letter, because the grammar makes use
+     ;; of non letters token and this would hide them. Other
+     ;; exception: Ltac things like "match" and "let' that need to be
+     ;; recognized as such by the grammar.
+     ((and (coq-is-at-command-real-start)
+           (> (length tok) 0)
+           (not (member tok '("match" "lazymatch" "let"))) ;; match are already captured
+           (or (string= "Lu" (get-char-code-property (aref tok 0) 'general-category))
+               (string= "Ll" (get-char-code-property (aref tok 0) 'general-category))))
+      "Com start")
+
      (tok))))
 
 
@@ -905,6 +949,9 @@ Lemma foo: forall n,
   :type 'boolean
   :group 'coq)
 
+(make-variable-buffer-local 'coq-indent-box-style)
+
+
 (defun coq-indent-safep (indent)
   (>= indent 0))
 
@@ -970,14 +1017,71 @@ Typical values are 2 or 4."
   :group 'coq
   :safe #'coq-indent-safep)
 
-;; - TODO: remove tokens "{ subproof" and "} subproof" but they are
-;;         needed by the lexers at a lot of places.
-;; - FIXME: This does not know about Notations.
-;; - TODO Actually there are two grammars: one at script level, for
-;;   indenting each command with respect to the previous commands, and
-;;   a standard one inside commands. Separating the two grammars would
-;;   greatly simplify this file. We should ask Stefan Monnier how to
-;;   have two grammars with smie.
+
+
+;; smie grammar. General Remarks.
+
+;; 1. One oddity (a standard one IIUC) is that the "command end token"
+;; is considerd a separator. So any command is the child of the
+;; previous one. This may lead to strange things wrt to indentation if
+;; we don't take care. For instance the following script
+;:;
+;; Com1 .(1)
+;; Definition foo := bar .(2)
+;; ...
+;; could easily lead to the grammar tree
+;;
+;;                        __.(2)
+;;                    .(1)      \
+;;                  /      \     ...
+;;                 /        \
+;;             Com1        :=
+;;                       /     \
+;;                  Def foo    bar
+;;
+;; which means that "(1)" is the parent of ":=", which is the parent
+;; of "Def foo". This leads to hell. We need Def to be the parent. But
+;; there are hundreds of commands in coq. so we adopt the policy below.
+;;
+;; 2. the lexer tries to always treat the first word of a command as a
+;; dstinguished token "Com start". And a command is of the form ("Com
+;; start" exp) in smie grammar. This way the top-node of a command is
+;; always this token.
+;;
+;; This way the above script is parsed as:
+;;
+;;                        __.(2)
+;;                    .(1)      \
+;;                  /      \     ...
+;;                 /        \
+;;             Com1     Com start
+;;                          |
+;;                         :=
+;;                       /    \
+;;                     foo    bar
+;;
+;; which is much better. Indenting *inside* a command never looks
+;; above its own "Com start". This makes indentation rules much
+;; simpler, and hopefully speeds up things too since in practice it
+;; means indentation never inspect too far.
+;;
+;; 3. The only exception to "Com start" token at command start is
+;; structuring commands like "Proof" "Module", "{ subproof", bullets,
+;; goal selectors.
+;;
+;; 4. All non-word tokens (in particular bullets) are also not seen as
+;; "Com start". Thus user-defined commands (or tactics) starting with
+;; a non-word token will probably break indentation.
+;;
+;; 5. KNOWN BUGS: This does not know about Notations, but users can
+;; add new syntax for already defined tokens.
+;;
+;; 6. BUGS: probably dozens of.
+;;
+;; TODO: factorize infix operators into a series of "opxx" where "xx"
+;; is the coq grammar priority. users could then add there own infix
+;; operators in a consistent way.
+
 (defconst coq-smie-grammar
   (smie-prec2->grammar
    (smie-bnf->prec2
@@ -994,7 +1098,6 @@ Typical values are 2 or 4."
        ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp)
        ("quantif exists" exp ", quantif" exp)
        ("forall" exp ", quantif" exp)
-;;;
        (exp "<- monadic" exp) (exp ";; monadic" exp)
        ("(" exp ")") ("{|" exps "|}") ("{" exps "}")
        (exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp)
@@ -1008,11 +1111,14 @@ Typical values are 2 or 4."
        (exp "+" exp) (exp "-" exp)
        (exp "*" exp) (exp "&&" exp)
        (exp "^" exp)
-       (exp ": ltacconstr" exp)(exp ". selector" exp))
+       (exp ": ltacconstr" exp)(exp ". selector" exp)
+       ("Com start" exp)
+       )
+      
       ;; Having "return" here rather than as a separate rule in `exp' causes
       ;; it to be indented at a different level than "with".
       (matchexp (exp) (exp "as match" exp) (exp "in match" exp)
-		(exp "return" exp) )
+		(exp "return match" exp) )
       (exps (affectrec) (exps "; record" exps))
       (affectrec (exp ":= record" exp))
       (assigns  (exp ":= let" exp) (exp "<- monadic" exp))
@@ -1065,29 +1171,33 @@ Typical values are 2 or 4."
       (assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet")
       (assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet")
       (assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet")
-      (assoc ".")
+      (left ".")
       (assoc "with inductive" "with fixpoint" "where"))
-    '((assoc ":= equations") (assoc ":= def" ":= inductive")
-      (assoc "|") (assoc "; equations") (assoc "=>") (assoc ":=")
-      (assoc "xxx provedby")
-      (assoc "as morphism") (assoc "with signature") (assoc "with match")
+    '((nonassoc "Com start") (assoc ":= equations")
+      (assoc ":= def" ":= inductive")
+      (left "|") (assoc "; equations") (assoc "=>") (assoc ":=")
+      (assoc "as morphism") (assoc "xxx provedby")
+      (assoc "with signature") (assoc "with match")
       (assoc "in let" "in monadic")
-      (assoc "in eval") (assoc "=> fun") (assoc ", quantif") (assoc "then")
+      (assoc "in eval") (left "=> fun") (left ", quantif") (assoc "then")
       (assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
-      (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
-      (assoc "|-") (assoc ":" ":<") (assoc ",")
+      (left "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
+      (assoc "|-") (assoc ":" ":<") (left ",")
       (assoc "else")
       (assoc "->") (assoc "<->")
-      (assoc "\\/") (assoc "&") (assoc "/\\")
-      (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>")
+      (left "\\/") (left "&" "/\\")
+      ;; FTR: left (instead of assoc) for "<" makes the hoare triple notation
+      ;; <{ .. }>\n exp \n<{ ... }> indent the two assertions at the same column.
+      (assoc "==") (assoc "=") (left "<" ">" "<=" ">=" "<>")
       (assoc "=?") (assoc "<=?") (assoc "<?")
       (assoc ";; monadic") (assoc "<- monadic")
       (assoc "^")
       (assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
-      (assoc "+") (assoc "-") (assoc "*")(assoc "&&")
+      ;; this make indentation as expected.
+      (left "+" "-") (left "*") (left "&&")
       (assoc ": ltacconstr") (assoc ". selector"))
-    '((assoc ":" ":<")  (assoc "<"))
-    '((assoc ". modulestart" "." ". proofstart") (assoc "Module def")
+    '((assoc ":" ":<") (left "<"))
+    '((assoc "Module def")
       (assoc "with module" "module nodecl") (assoc ":= module")
       (assoc ":= with module")  (assoc ":" ":<"))
     '((assoc ":= def") (assoc "; record") (assoc ":= record"))))
@@ -1143,17 +1253,38 @@ Typical values are 2 or 4."
   "Return non-nil if PARENT-POS is on same line as CHILD-POS."
   (= (line-number-at-pos parent-pos) (line-number-at-pos child-pos)))
 
-(defcustom coq-indent-basic nil
+(defcustom coq-indent-basic 2
   "Basic indentation step.
 If nil, default to `proof-indent' if it exists or to `smie-indent-basic'."
   :group 'coq-mode
   :type '(choice (const :tag "Fallback on global settings" nil)
           integer))
 
-
-;; Debugging smie parent token, needs the highlight library
-;;and something like this in .emacs:
-;; (require 'highlight)
+;; otherwise there are some glitches
+(setq smie-indent-basic coq-indent-basic)
+
+;;;;;;;;;; DEBUG CODE ;;;;;;
+;; smie-config-show-indent is sufficient most of the time.
+
+(defun coq-debug-smie--parent (point parent &optional num)
+  ;;refresh highlighting? Not a good idea since this is called several times.
+  ;;(hlt-unhighlight-region)
+  (let* ((beg (if (listp (car parent)) (caar parent) (car parent)))
+         (end (cadr parent))
+         (regi (list (list beg end)))
+         (tok (caddr parent))
+         (face (cond
+                ((equal num 1) 'hlt-regexp-level-1)
+                ((equal num 2) 'hlt-regexp-level-2)
+                (t 'hlt-regexp-level-1))))
+    ;; uncomment to see visually the region
+    ;;(and parent (hlt-highlight-regions regi face))
+    ;;(when end (hlt-highlight-regions (list (list end (+ end 1))) 'hlt-regexp-level-1))
+    ;; and the point considered
+    (hlt-highlight-regions (list (list point (+ point 1))) 'holiday)))
+
+;; Debugging smie rules calls, needs the highlight library and
+;; something like this in .emacs: (require 'highlight)
 ;; (custom-set-faces '(highlight ((((type x) (class color) (background light)) (:background "Wheat")))))
 (defun coq-show-smie--parent (parent token parent-token &optional num msg)
   (ignore-errors
@@ -1167,248 +1298,133 @@ If nil, default to `proof-indent' if it exists or to `smie-indent-basic'."
                  ((equal num 2) 'hlt-regexp-level-2)
                  (t 'hlt-regexp-level-1))))
      (and parent (hlt-highlight-regions regi face)))))
+;;;;;;;;;; END DEBUG CODE ;;;;;;;;;;;;
+
+(defun coq-indent-categorize-token-after (tk)
+  "Factorize tokens behaving the same \"smie-rules\"-wise (kind:after)."
+  (cond
+   ((coq-is-bullet-token tk) "after bullet")
+   ((member tk '("with" ":" "by" "in tactic" "as" ",")) "tactic infix")
+   ((member tk '("<:" "<+" "with module")) "modulespec infix") ;;  ":= inductive" ":= module" and other ":= xxx"
+   ((string-prefix-p ":= " tk) "after :=")
+   ((member tk '(". proofstart" ". modulestart")) "dot script parent open")
+   ;; by default we pass the token name, but maybe it would be safer
+   ;; to simply fail, so that we detect missing tokens in this function?
+   (t tk)))
+
+(defun coq-indent-categorize-token-before (tk)
+  "Factorize tokens behaving the same \"smie-rules\"-wise (kind:after)."
+  (cond
+   ((member tk '(". proofstart" ". modulestart")) "dot script parent open")
+   ((member tk '(":" "by" "in tactic" "as" "with" ",")) "tactic infix")
+   ((string-prefix-p ":= " tk) "before :=")
+
+   ;; by default we pass the token name, but maybe it would be safer
+   ;; to simply fail, so that we detect missing tokens in this function?
+   (t tk)))
+
+
+;; ";" is a usual operator, with no indentation
+;; it would be like this;
+;;  foo.
+;;  foo ;
+;;  bar ;
+;;  bar.
+;;  foo.
+;; which is confusing. So we indent the first ";" of a sequence
+;; if not already inside an ltacdef of parenthesized tactic:
+;; foo ;
+;;   tac ; <--- indented
+;;   tac ; <--- no indent
+;;   [ tac2 ;
+;;     tac1 ; <-- no indentation here
+;;     now ( tac3 ;  <- neither here
+;;           tac5) ;
+;;   ]
+(defun coq-smie-ltac-semicol-indent-first (parent-semicol)
+  (and coq-indent-semicolon-tactical (not parent-semicol)
+       (not (coq-smie-is-ltacdef))
+       (not (coq-smie-is-inside-parenthesized-tactic))))
+
+
+;; this should be called if we already know that parent is a quantif.
+(defun coq--prev-quantif-at-indent-p ()
+  (save-excursion
+    (coq-smie-search-token-backward '("forall" "quantif exists"))
+    (equal (current-column) (current-indentation))))
 
-
+;; Reminder: (smie-rule-separator kind) only works for *parenthesized* enumerations.
+;; and ":= inductive" is not considered a parenthesis so "|" needs special hack
+;; below. "," for tuples and for tac args cannot be distinguished, so it cannot be
+;; treated like this either.
 
 (defun coq-smie-rules (kind token)
   "Indentation rules for Coq.  See `smie-rules-function'.
 KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
-  (pcase kind
-     (`:elem (pcase token
-	       (`basic (or coq-indent-basic
-                           (bound-and-true-p proof-indent)
-                           smie-indent-basic))))
-     (`:close-all t)
-     (`:list-intro
-      (or (member token '("fun" "forall" "quantif exists" "with"))
-	  ;; We include "." in list-intro for the ". { .. } \n { .. }" so the
-	  ;; second {..} is aligned with the first rather than being indented as
-	  ;; if it were an argument to the first.
-	  ;; FIXME: this gives a strange indentation for ". { \n .. } \n { .. }"
-;	  (when (or (coq-is-bullet-token token)
-;		    (coq-is-dot-token token)
-;		    (member token '("{ subproof")))
-;	    (forward-char 1) ; skip de "."
-;	    (equal (coq-smie-forward-token) "{ subproof"))
-	  ))
-     (`:after
-      ;;(coq-show-smie--parent smie--parent smie--token (smie-indent--parent) 1 "AFTER")
-      (cond
-       ;; Override the default indent step added because of their presence
-       ;; in smie-closer-alist.
-       ((or (coq-is-bullet-token token)
-	    (member token '(":" ":=" ":= with" ":= def" ":= equations"
-			    "by" "in tactic" "<:" "<+" ":= record"
-			    "with module" "as" ":= inductive" ":= module" )))
-	2)
-
-       ((equal token "with match") coq-match-indent)
-
-       ;; Inductive foo ...
-       ;; ...
-       ;; with
-       ;;   bar  <-- indent this by 2
-       ;; TODO: have this optional?
-       ((equal token "with inductive")
-	(if (smie-rule-parent-p "with inductive")
-	    0
-	  2)) 
-
-       ((equal token "with") 2)  ; add 2 to the column of "with" in the children
-
-       ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;XXXXXXXXXXXXXXXXXXXXXXXx
-       ((and (member token '("{" "{|"))
-             (smie-rule-prev-p ":=" ":= def")
-             (not coq-indent-box-style))
-        (save-excursion
-          (smie-backward-sexp t)
-          (cons 'column (+ 2 (smie-indent-virtual)))))
-
-
-       ;;; the ";" tactical ;;;
-       ;; ";" is a usual operator, with no indentation
-       ;; it would be like this;
-       ;;  foo.
-       ;;  foo ;
-       ;;  bar ;
-       ;;  bar.
-       ;;  foo.
-       ;; which is confusing. So we indent the first ";" of a sequence
-       ;; if not already inside an ltacdef of parenthesized tactic:
-       ;; foo ;
-       ;;   tac ; <--- indented
-       ;;   tac ; <--- no indent
-       ;;   [ tac2 ;
-       ;;     tac1 ; <-- no indentation here
-       ;;     now ( tac3 ;  <- neither here
-       ;;           tac5) ;
-       ;;   ]
-       ((equal token "; tactic")
-	(if (and (smie-rule-hanging-p)
-		 coq-indent-semicolon-tactical
-		 (not (coq-smie-is-ltacdef))
-		 (not (coq-smie-is-inside-parenthesized-tactic))
-		 (or (not (smie-rule-parent-p "; tactic"))
-                     ;; FIXME: Don't depend on SMIE's internals!
-		     (and (boundp 'smie--parent)
-                          smie--parent
-			  (coq-smie--same-line-as-parent
-			   (nth 1 smie--parent) (point)))))
-	    coq-indent-semicolon-tactical
-	  nil))
-
-       ((member token '("in let" "in monadic")) (smie-rule-parent))
-
-       ((equal token "} subproof")
-        (smie-rule-parent))
-
-       ;; proofstart is a special hack, since "." should be used as a
-       ;; separator between commands, here it is recognized as an open
-       ;; parenthesis, hence the current command (C) ending with "."
-       ;; is not recognized as correctly terminated. The "parent"
-       ;; computed by smie is therefore wrong and default indetation
-       ;; is broken. We fix this by indenting from the real-start of
-       ;; the command terminated by ". proofstart".
-       ((equal token ". proofstart")
-	(save-excursion (forward-char -1) (coq-find-real-start)
-			`(column . ,(+ coq-indent-proofstart (current-column)))))
-       ((equal token ". modulestart")
-	(save-excursion (forward-char -1) (coq-find-real-start)
-			`(column . ,(+ coq-indent-modulestart (current-column)))))))
-
-     (`:before
-      ;(coq-show-smie--parent smie--parent smie--token (smie-indent--parent) 2 "BEFORE")
-      (cond
+  (let ((boxed coq-indent-box-style))
+    ;; smie-rule... short synonyms
+    (cl-flet ((parent-p (&rest x) (apply 'smie-rule-parent-p x))
+              (parent (&optional x) (smie-rule-parent x))(hang-p () (smie-rule-hanging-p)))
+      (pcase (cons kind token)
+        (`(,_ . (or "; record")) (smie-rule-separator kind)) ;; see also the "before" rule
+        (`(:elem . basic) (or coq-indent-basic (bound-and-true-p proof-indent) 2))
+        (`(:elem . arg) nil)
+        (`(:close-all . ,_) t)
+        (`(:list-intro . ,_) (member token '("fun" "forall" "quantif exists"
+                                             "with" "Com start")))
+        (`(:after . ,_) ;; indent relative to token (parent of token at point).
+         (pcase (coq-indent-categorize-token-after token)
+           ("} subproof" 0) ;;shouldn't be captured by (:elem . args)?
+           ;; decrement indentation when hanging 
+           ((and (or "tactic infix" "after :=") (guard (or (hang-p) (smie-rule-bolp)))) 0)
+           ((and "->" (guard (hang-p))) 0) ((or ":=" "with inductive") 2)
+           ((or "." "; equations" "in let" "in monadic" ";; monadic") 0)
+           ((and "; tactic" (guard (hang-p)) (guard (not (parent-p "Com start")))) 0)
+           ("; tactic" 2);; only applies "after" so when ";" is alone at its line
+           ((guard (string-match "^[^][:alnum:](){}\[]" token)) 2); guessing infix operator.
+           ;;((guard (and (message "DEFAULTING") nil)) nil)
+           ))
+        (`(:before . ,_) ; indent token at point itself
+         (let* ((cat (coq-indent-categorize-token-before token))
+                (real-start-col (save-excursion (coq-find-real-start) (current-column))))
+           (pcase cat
+             ;; indenting the ". modulestart" itself, which is a prenthesizing cmd
+             ("dot script parent open" `(column . ,real-start-col))
+             ;; special case for equations, so that "| xxx\n :=" is indented nicely
+             ((and ":=" (guard (and (not (hang-p)) (parent-p "|")))) 4)
+             ("before :=" (parent 2)) ;; ":= xxx" always introduced by a parent
+             ("tactic infix" (parent 2))
+             ("|" (cond ((parent-p ":= inductive" ":= equations") -2)
+                        (t 0)));((parent-p "|") 0)
+             ;; align quantifiers with the previous one
+             ((and(or "forall" "quantif exists")(guard (parent-p "forall" "quantif exists")))
+              (parent))
+             ((and(or "fun")(guard (parent-p "fun"))) (parent))
+             ;; indent on level after a ";" but only at command level.
+             ((and "; tactic" (guard (parent-p "Com start"))) (parent))
+             ("; record" 0); is also a smie-rule-separator
+             ;; VIRTUAL INDENTATION for "unboxed" indentation: we are in the "before"
+             ;; section, but we compute the indentation for a token NOT appearing at
+             ;; beginning of line. This happens when not indenting the token itself but
+             ;; rather querying its virtual indentation to compute indentation of another
+             ;; (child) token. unbox ==> indent relative to parent.
+             ;; unboxed indent for "{" not at bol:
+             ((and (or "{ subproof" "[" "{") (guard (not (smie-rule-bolp))))
+              (cond 
+               ((smie-rule-prev-p "} subproof" "]" "}") (parent 0))
+               (t (parent 2))))
+             ;; unboxed indent for quantifiers (if coq-indent-box-style non nil)
+             ((and (or "forall" "quantif exists") (guard (not boxed))
+                   (guard (not (smie-rule-bolp))) )
+              (parent coq-smie-after-bolp-indentation))
+             ;;((guard (and (message "DEFAULTING") nil)) nil)
+             )))))))
 
 
-       ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;XXXXXXXXXXXXXXXXXXXXXXXx;;;;;;;;;;;;;;
-       ;; trying to indent "{" at the end of line for records, but the
-       ;; parent is not what I think.
-       ;; ((and (member token '("{" "{|"))
-       ;;       (not coq-indent-box-style))
-       ;;  (if (smie-rule-bolp) 2 0))
-       ;(and (zerop (length tok)) (member (char-before) '(?\{ ?\})))
-       ((and (zerop (length token))
-             (looking-back "}" (1- (point))) ;; "|}" useless when looking backward
-             (not coq-indent-box-style))
-        (smie-backward-sexp)
-        (smie-backward-sexp t)
-        (smie-indent-virtual)
-        )
-
-       ;; "with" is also in the :list-intro rules and in :after.
-       ((equal token "with")
-        ;; Hack: We know that "with" is linked to the first word of
-        ;; the current atomic tactic. This tactic is the parent, not
-        ;; the "." of the previous command.
-        `(column . ,(+ 2 (coq-find-with-related-backward))))
-
-       ((equal token "with module")
-	(if (smie-rule-parent-p "with module")
-	    (smie-rule-parent)
-	  (smie-rule-parent 2)))
-
-       ((member token '("in tactic" "as" "by"))
-	(cond
-	 ((smie-rule-parent-p "- bullet" "+ bullet" "* bullet"
-			      "-- bullet" "++ bullet" "** bullet"
-			      "--- bullet" "+++ bullet" "*** bullet"
-			      "---- bullet" "++++ bullet" "**** bullet"
-			      "{ subproof" ". proofstart")
-	  (smie-rule-parent 4))
-	 ((smie-rule-parent-p "in tactic") (smie-rule-parent))
-	 (t (smie-rule-parent 2))))
-
-       ((equal token "as")
-	(if (smie-rule-parent-p "in tactic") (smie-rule-parent) 2))
-
-       ((equal token "as morphism") (smie-rule-parent 2))
-       ((member token '("xxx provedby" "with signature"))
-	(if (smie-rule-parent-p "xxx provedby" "with signature")
-	    (smie-rule-parent)
-	  (smie-rule-parent 4)))
-
-
-       ;; This applies to forall located on the same line than "Lemma"
-       ;; & co. This says that "if it *were* be on the beginning of
-       ;; line" (which it is not) it would be indented of 2 wrt
-       ;; "Lemma". This never applies directly to indent the forall,
-       ;; but it is used to guess indentation of the next line. This
-       ;; allows fo the following indentation:
-       ;;  Lemma foo: forall x:nat,
-       ;;      x <= 0 -> x = 0.
-       ;; which refer to:
-       ;;  Lemma foo:
-       ;;    forall x:nat, <--- if it where on its own line it would be on column 2
-       ;;      x <= 0 -> x = 0. <--- therefore this is on column 4.
-       ;; instead of:
-       ;;  Lemma foo: forall x:nat,
-       ;;               x <= 0 -> x = 0.
-
-       ((and (member token '("forall" "quantif exists"))
-	     (not coq-indent-box-style)
-	     (not (smie-rule-bolp)))
-	(smie-rule-parent coq-smie-after-bolp-indentation))
-
-
-
-       ((and (member token '("forall" "quantif exists"))
-	     (smie-rule-parent-p "forall" "quantif exists"))
-	(if (save-excursion
-	      (coq-smie-search-token-backward '("forall" "quantif exists"))
-	      (equal (current-column) (current-indentation)))
-	    (smie-rule-parent)
-	  (smie-rule-parent 2)))
-
-
-       ;; This rule allows "End Proof" to align with corresponding ".
-       ;; proofstart" PARENT instead of ". proofstart" itself
-       ;;  Typically:
-       ;;    "Proof" ". proofstart"
-       ;;    "Qed" <- parent is ". proofstart" above
-       ;; Align with the real command start of the ". xxxstart"
-       ((member token '(". proofstart" ". modulestart"))
-	(save-excursion (coq-find-real-start)
-			`(column . ,(current-column))))
-
-       ((or (member token '(":= inductive" ":= def" ":= equations" ":="))
-            (and (equal token ":") (smie-rule-parent-p ".")))
-        (let ((pcol
-               (save-excursion
-                 ;; Indent relative to the beginning of the current command
-                 ;; rather than relative to the previous command.
-                 (smie-backward-sexp token)
-                 ;; special case: if this ":=" corresponds to a "with
-                 ;; foo", then the previous smie-backward-sexp stopped
-                 ;; between "with" and "foo" (because "with inductive"
-                 ;; and co are considered as ".", maybe this is the
-                 ;; problem), but we want to indent from the column of
-                 ;; "with" instead
-                 (let ((col1 (current-column)))
-                   (if (equal (coq-smie-backward-token) "with inductive")
-                       (current-column)
-                     col1)
-                   ))))
-          `(column . ,(if (smie-rule-hanging-p) pcol (+ 2 pcol)))))
-
-       ((equal token "|")
-	(cond
-         ;; ":= equations" and "; record" are for Equations plugin
-         ((smie-rule-parent-p "with match" ":= equations" "; record")
-	  (- (funcall smie-rules-function :after "with match") 2))
-         ;; This is also for Equations plugijns, but happens at first
-         ;; line if a pattern matching and it is ugly to have the "|"
-         ;; at the saem column than "{"
-         ((smie-rule-parent-p "{")
-	  (funcall smie-rules-function :after "with match"))
-	 ((smie-rule-prev-p ":= inductive")
-	  (- (funcall smie-rules-function :after ":= inductive") 2))
-	 (t (smie-rule-separator kind))))))
-     ))
 
 ;; No need of this hack anymore?
 ;;       ((and (equal token "Proof End")
-;;             (smie-rule-parent-p "Module" "Section" "goalcmd"))
+;;             (parent-p "Module" "Section" "goalcmd"))
 ;;        ;; ¡¡Major gross hack!!
 ;;        ;; This typically happens when a Lemma had no "Proof" keyword.
 ;;        ;; We should ideally find some other way to handle it (e.g. matching Qed
@@ -1418,7 +1434,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
 ;;        ;; when parsing backward.
 ;;        ;; FIXME: This is fundamentally very wrong, but it seems to work
 ;;        ;; OK in practice.
-;;        (smie-rule-parent 2))
+;;        (parent 2))
 
 
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index afcbd3166..b8b498a22 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1385,7 +1385,7 @@ different."
 (defconst coq-command-prefix-regexp "\\(Local\\s-\\|Global\\s-\\|#[[][^]]*[]]\\)")
 ;; FIXME: incomplete
 
-(defun coq-add-command-prefix (reg) (concat "\\(" coq-command-prefix-regexp "\\)?" (mapconcat #'identity coq-keywords-defn "\\|")))
+(defun coq-add-command-prefix (reg) (concat "\\(" coq-command-prefix-regexp "\\)?" (mapconcat #'identity reg "\\|")))
 
 (defconst coq-command-decl-regexp (coq-add-command-prefix coq-keywords-decl))
 (defconst coq-command-defn-regexp (coq-add-command-prefix coq-keywords-defn))
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 2a0d5e478..17bf4819c 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -342,7 +342,7 @@ Module X.
 
         match goal with
         | ?g := _:rec |- ?a /\ ?b => split
-              | _ => fail
+        | _ => fail
         end.
 
         Fail

From 87070228d798611e6cbe3af0016d07d044dc221c Mon Sep 17 00:00:00 2001
From: Pierre COURTIEU <pierre.courtieu@cnam.fr>
Date: Thu, 26 Aug 2021 19:36:49 +0200
Subject: [PATCH 3/4] Indentation testing CI ready (hopefully).

---
 ci/test-indent/Makefile                       | 22 +++++++++++++++++++
 ci/test-indent/coq-test-indent.sh             | 12 +++++++---
 ...{indent_equations.v => indent-equations.v} |  0
 .../{indent_monadic.v => indent-monadic.v}    |  0
 ci/test-indent/tests.sh                       |  1 +
 5 files changed, 32 insertions(+), 3 deletions(-)
 create mode 100644 ci/test-indent/Makefile
 rename ci/test-indent/{indent_equations.v => indent-equations.v} (100%)
 rename ci/test-indent/{indent_monadic.v => indent-monadic.v} (100%)

diff --git a/ci/test-indent/Makefile b/ci/test-indent/Makefile
new file mode 100644
index 000000000..5aa999ac7
--- /dev/null
+++ b/ci/test-indent/Makefile
@@ -0,0 +1,22 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2021  Pierre Courtieu
+# 
+# Authors: Pierre Courtieu
+# Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+# 
+# License:     GPL2+ (GNU GENERAL PUBLIC LICENSE)
+
+TESTS:=$(wildcard indent-*.v)
+INDENTED:=$(subst indent-,indented_indent-, $(TESTS))
+
+all: $(INDENTED)
+
+indented_%.v: %.v
+	@echo "### testing indentation of $<..."
+	@./coq-test-indent.sh $<
+
+.PHONY: clean
+
+clean:
+	rm -f indented_indent*
diff --git a/ci/test-indent/coq-test-indent.sh b/ci/test-indent/coq-test-indent.sh
index 7204d002d..2f3539792 100755
--- a/ci/test-indent/coq-test-indent.sh
+++ b/ci/test-indent/coq-test-indent.sh
@@ -1,3 +1,4 @@
+#!/bin/bash
 
 # This script should be launched from its own directory, so that file
 # coq-test-indent.el is accessible.
@@ -24,14 +25,19 @@ emacs -q -batch --eval "(progn (load-file \"coq-test-indent.el\") (launch-test \
 # echo "grep \"INDENT CHANGED\" $INDENTEDTESTFILE"
 # grep "INDENT CHANGED" $INDENTEDTESTFILE
 echo -n " diff -q $TESTFILE $INDENTEDTESTFILE..."
-diff -q $TESTFILE $INDENTEDTESTFILE > /dev/null
-if [[ $? == 1 ]] ;
+diff -q $TESTFILE $INDENTEDTESTFILE
+if [[ "$?" == 1 ]] ;
 then echo " DIFFERENCES FOUND" 
+     diff -u $TESTFILE $INDENTEDTESTFILE
      printf "${RED} TEST FAILURE ***${NC}\n"
-     echo "  *** details can be seen with:"
+     echo "  *** details can be seen by reproducing the tests:"
+     echo "  *** cd ci/test-indent"
+     echo "  *** make"
      echo "  ***  diff --side-by-side --suppress-common-lines $TESTFILE $INDENTEDTESTFILE"
      echo "  *** or graphically: "
      echo "  ***  meld $TESTFILE $INDENTEDTESTFILE"
+     exit 1 # Make the test program fail, so that CI knows.
 else echo "NO DIFFERENCE"
      printf "${GREEN} TEST SUCCESS *** ${NC}\n"
+     exit 0
 fi
diff --git a/ci/test-indent/indent_equations.v b/ci/test-indent/indent-equations.v
similarity index 100%
rename from ci/test-indent/indent_equations.v
rename to ci/test-indent/indent-equations.v
diff --git a/ci/test-indent/indent_monadic.v b/ci/test-indent/indent-monadic.v
similarity index 100%
rename from ci/test-indent/indent_monadic.v
rename to ci/test-indent/indent-monadic.v
diff --git a/ci/test-indent/tests.sh b/ci/test-indent/tests.sh
index 9dcd5c095..ef2c23e14 100755
--- a/ci/test-indent/tests.sh
+++ b/ci/test-indent/tests.sh
@@ -1,3 +1,4 @@
+#!/bin/bash
 
 
 

From 260a6a2cd7581aa125770e6d8bce5befc7374e29 Mon Sep 17 00:00:00 2001
From: Pierre COURTIEU <pierre.courtieu@cnam.fr>
Date: Fri, 27 Aug 2021 10:33:21 +0200
Subject: [PATCH 4/4] Adding the CI for indentation.

---
 .github/workflows/test.yml | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 7fcc4733a..9874fa4dd 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -223,3 +223,32 @@ jobs:
             sudo chown -R coq:coq ./ci
             make -C ci/simple-tests all
           endGroup
+
+  # Run indentation tests in ci/test-indent on all supported emacs
+  # versions without coq installed.
+  test-indent:
+    runs-on: ubuntu-latest
+
+    strategy:
+      matrix:
+        emacs_version:
+          - 25.1
+          - 25.2
+          - 25.3
+          - 26.1
+          - 26.2
+          - 26.3
+          - 27.1
+      max-parallel: 4
+      # don't cancel all in-progress jobs if one matrix job fails:
+      fail-fast: false
+
+    steps:
+    - uses: actions/checkout@v2
+
+    - uses: purcell/setup-emacs@master
+      with:
+        version: ${{ matrix.emacs_version }}
+
+    - run: emacs --version
+    - run: make -C ci/test-indent