From 1f2cc4026cd5e977979ff1507fd5fa0d96e1a92f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 25 Dec 2015 06:08:29 +0100
Subject: Moving the ad hoc interpretation of "intros" as "intros **" from
 tacinterp.ml to g_tactic.ml4 so as to leave room for "IntroPattern []" to
 mean "no introduction".

---
 parsing/g_tactic.ml4 | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a197e0209c..31125e37cf 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -281,6 +281,9 @@ GEXTEND Gram
   intropatterns:
     [ [ l = LIST0 nonsimple_intropattern -> l ]]
   ;
+  ne_intropatterns:
+    [ [ l = LIST1 nonsimple_intropattern -> l ]]
+  ;
   or_and_intropattern:
     [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> tc
       | "()" -> [[]]
@@ -532,7 +535,10 @@ GEXTEND Gram
   simple_tactic:
     [ [
       (* Basic tactics *)
-        IDENT "intros"; pl = intropatterns -> TacAtom (!@loc, TacIntroPattern pl)
+        IDENT "intros"; pl = ne_intropatterns ->
+          TacAtom (!@loc, TacIntroPattern pl)
+      | IDENT "intros" ->
+          TacAtom (!@loc, TacIntroPattern [!@loc,IntroForthcoming false])
       | IDENT "intro"; id = ident; hto = move_location ->
 	  TacAtom (!@loc, TacIntroMove (Some id, hto))
       | IDENT "intro"; hto = move_location -> TacAtom (!@loc, TacIntroMove (None, hto))
-- 
cgit v1.2.3