Removing the special status of generic arguments defined by Coq itself.

This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.

1 files changed, 18 insertions, 0 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 8215e785ab..d33ec91f9d 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -55,6 +55,14 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ ] -> [ true ]
 END
 
+let pr_int _ _ _ i = Pp.int i
+
+let _natural = Pcoq.Prim.natural
+
+ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int
+| [ _natural(i) ] -> [ i ]
+END
+
 let pr_orient = pr_orient () () ()
 
 
@@ -122,6 +130,8 @@ let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
 let glob_glob = Tacintern.intern_constr
 
+let pr_lconstr _ prc _ c = prc c
+
 let subst_glob = Tacsubst.subst_glob_constr_and_expr
 
 ARGUMENT EXTEND glob
@@ -139,6 +149,14 @@ ARGUMENT EXTEND glob
   [ constr(c) ] -> [ c ]
 END
 
+let l_constr = Pcoq.Constr.lconstr
+
+ARGUMENT EXTEND lconstr
+    TYPED AS constr
+    PRINTED BY pr_lconstr
+  [ l_constr(c) ] -> [ c ]
+END
+
 ARGUMENT EXTEND lglob
     PRINTED BY pr_globc