From 0fdb1ae633baeb9afb07bbd8632bece5976f95f2 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 16 Oct 2020 09:14:11 +0200
Subject: Fix #514 + support for named goal selector.

It was hard to separate this too fixes (same regexps).
---
 coq/ex/indent.v | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

(limited to 'coq/ex')

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'.
-- 
cgit v1.2.3