Fix #514 + support for named goal selector.

It was hard to separate this too fixes (same regexps).

1 files changed, 23 insertions, 2 deletions

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index e93616c8..72a3c201 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -4,8 +4,8 @@ Notation "[ ]" := nil : list_scope.
 Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
 
 Require Import Arith.
-
-Definition arith1:
+Open Scope nat_scope.
+Definition arith1:=
   1 + 3 *
       4.
 
@@ -190,6 +190,27 @@ Module M1.
   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'.