[nongnu] elpa/proof-general b550e90 1/4: Fix #574 indent of ltac "letins" pattern.

[ELPA Syncer]

branch: elpa/proof-general
commit b550e906a268cc5e543cd409d79180805c0958ab
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Matafou@users.noreply.github.com>

    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 2c3b577..88e3375 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 b8571d2..afcbd31 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 72a3c20..2a0d5e4 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