From ab7639ed91da9726f5248d9939db70df9ea18282 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 21 Dec 2018 14:14:05 -0800
Subject: Move and rewrite documentation for intro patterns that was under the
 intros tactic to its own subsection.  Add grammar and examples.

---
 plugins/ltac/g_tactic.mlg | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 46ea3819ac..7bf705ffeb 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -287,10 +287,10 @@ GRAMMAR EXTEND Gram
     [ [ c = smart_global; nl = occs -> { (nl,c) } ] ]
   ;
   intropatterns:
-    [ [ l = LIST0 nonsimple_intropattern -> { l } ] ]
+    [ [ l = LIST0 intropattern -> { l } ] ]
   ;
   ne_intropatterns:
-    [ [ l = LIST1 nonsimple_intropattern -> { l } ] ]
+    [ [ l = LIST1 intropattern -> { l } ] ]
   ;
   or_and_intropattern:
     [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc }
@@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram
       | "?" -> { IntroAnonymous }
       | id = ident -> { IntroIdentifier id } ] ]
   ;
-  nonsimple_intropattern:
+  intropattern:
     [ [ l = simple_intropattern -> { l }
       | "*"  -> { CAst.make ~loc @@ IntroForthcoming true }
       | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ]
@@ -534,6 +534,8 @@ GRAMMAR EXTEND Gram
           { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
       | IDENT "eintros"; pl = ne_intropatterns ->
           { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) }
+      | IDENT "eintros" ->
+          { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,[CAst.make ~loc @@IntroForthcoming false])) }
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) }
-- 
cgit v1.2.3