branch: elpa/proof-general
commit b550e906a268cc5e543cd409d79180805c0958ab
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <mata...@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
