Merge pull request #861 from Matafou/fix-named-goals

Fixing support for named goal.

Author: Matafou

ci/coq-tests.el

@@ -518,7 +518,7 @@ For example, COMMENT could be (*test-definition*)"
        (while (setq type (funcall proof-script-parse-function))
          (setq cpt (+ 1 cpt))
          (should (equal type 'cmd)))
-       (should (equal cpt 17))))))
+       (should (equal cpt 31))))))
 
 
 (provide 'coq-tests)

ci/test-indent/indent-commands-boxed.v

@@ -252,6 +252,15 @@ Module Mod.
       idtac.
       idtac.
     }
+    [foo.bar]:{
+      idtac.
+      - idtac.
+        idtac. {
+          idtac.
+          idtac.
+        }
+        idtac.
+    }
     [foo]:{
       idtac.
       - idtac.

ci/test-indent/indent-commands.v

@@ -249,6 +249,15 @@ Module Mod.
       idtac.
       idtac.
     }
+    [foo.bar]:{
+      idtac.
+      - idtac.
+        idtac. {
+          idtac.
+          idtac.
+        }
+        idtac.
+    }
     [foo]:{
       idtac.
       - idtac.

ci/test_command_parsing.v

@@ -4,19 +4,32 @@ Definition Bar := nat.
 From elpi Require Import elpi.
 
 
-Lemma le_prop: forall n m p:entier, le n m -> le m p -> le n p.
+Lemma le_prop: forall n m p:nat, le n m -> le m p -> le n p.
 Proof.
   intros n m p. 
   intro H.
   revert p.
   induction H;intros.
   - assumption.
   - { + apply IHle.
-        apply le_Suuc_a_gauche.
+        apply le_S_n.
+        apply le_S.
         assumption. }
 Qed.
 
-
+(* named goals are in rocq >= 9.2,  *)
+Open Scope bool_scope.
+Set Generate Goal Names.
+Goal forall a b, a && b = b && a.
+Proof.
+  intros a b. 
+  destruct a,b.
+  [true.true]: {
+    cbn. reflexivity. }
+  [true.false]: {
+    cbn. reflexivity.
+  }
+Admitted.
 
 Elpi Tactic show.
 Elpi Accumulate lp:{{

coq/coq-indent.el

@@ -44,8 +44,8 @@ No context checking.")
 
 ;; goal selectors are of two forms;
 ;; 2:
-;; [goalname]:
-(defconst coq-goal-selector-regexp "\\(?:[0-9]+\\|\\[\\w+\\]\\)\\s-*:\\s-*"
+;; [goalname]: where goalname may contain "." (at least)
+(defconst coq-goal-selector-regexp "\\(?:[0-9]+\\|\\[[^]]+\\]\\)\\s-*:\\s-*"
   "regexp of goal selector in coq.")
 
 ;;;;;;;;;;;;;;; FORWARD / BACKWARD REGEXP ;;;;;;;;;;;;;;;;;
@@ -385,6 +385,7 @@ Comments are ignored, of course."
    ;; TODO: looking-back is supposed to be slow. Find something else? 
    ((or (and (looking-at "{")(looking-back "[0-9]+\\s-*:\\s-*" nil t))
         (and (looking-at ":\\s-*{")(looking-back "[0-9]+\\s-*" nil t))
+        (and (looking-at ":\\s-*{")(looking-back "\[[^]]+\]\\s-*" nil t))
         (and (looking-at "[0-9]+:\\s-*{") nil t))
     (goto-char (match-beginning 0))     ; swallow goal selector
     (coq-empty-command-p))

coq/coq-smie.el

@@ -776,14 +776,14 @@ The point should be at the beginning of the command name."
            (save-excursion
              (forward-char -1)
              (if (and (looking-at "{")
-                      (looking-back "\\(\\[?\\w+\\]?\\s-*:\\s-*\\)" nil t))
+                      (looking-back coq-goal-selector-regexp nil t))
                  (goto-char (match-beginning 0)))
              (let ((nxttok (coq-smie-backward-token))) ;; recursive call
                (coq-is-cmdend-token nxttok))))
       (forward-char -1)
       (if (looking-at "}") "} subproof"
         (if (and (looking-at "{")
-                 (looking-back "\\(\\[?\\w+\\]?\\s-*:\\s-*\\)" nil t))
+                 (looking-back coq-goal-selector-regexp nil t))
             (goto-char (match-beginning 0)))
         "{ subproof"
         ))