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.

5 files changed, 20 insertions, 30 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 41e94914ee..82bc09519b 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -46,18 +46,16 @@ let has_extraarg l =
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (t, _, p) :: tl ->
-	<:expr<
-            (fun $lid:p$ ->
-               let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
-        >>
+    | ExtNonTerminal (t, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
     | ExtTerminal _ :: tl ->
 	<:expr< (fun _ -> $make tl$) >> in
   make (List.rev pil)
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
-  | ExtNonTerminal (_, g, _) -> mlexpr_of_prod_entry_key g
+  | ExtNonTerminal (_, g, _) ->
+    let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
+    mlexpr_of_prod_entry_key base g
 
 let rec make_prod = function
 | [] -> <:expr< Extend.Stop >>
@@ -174,7 +172,6 @@ let declare_vernac_argument loc s pr cl =
         (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) }
       >> ]
 
-open Pcoq
 open Pcaml
 open PcamlSig (* necessary for camlp4 *)
 
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 3946d5d2b9..c43ce15be2 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -47,31 +47,23 @@ let mlexpr_of_option f = function
 let mlexpr_of_ident id =
   <:expr< Names.Id.of_string $str:id$ >>
 
-let rec mlexpr_of_prod_entry_key = function
-  | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
-  | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >>
-  | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >>
-  | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
-  | Extend.Uentry e -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >>
+let rec mlexpr_of_prod_entry_key f = function
+  | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Uentry e -> <:expr< Pcoq.Aentry $f e$ >>
   | Extend.Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (CString.equal e "tactic");
     if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
     else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
 
-let type_entry u e =
-  let Pcoq.TypedEntry (t, _) = Pcoq.get_entry u e in
-  Genarg.unquote t
-
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s ->
   Genarg.ListArgType (type_of_user_symbol s)
 | Uopt s ->
   Genarg.OptArgType (type_of_user_symbol s)
-| Uentry e | Uentryl (e, _) ->
-  try type_entry Pcoq.uprim e with Not_found ->
-  try type_entry Pcoq.uconstr e with Not_found ->
-  try type_entry Pcoq.utactic e with Not_found ->
-  Genarg.ExtraArgType e
+| Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 837ec6fb02..712aa8509d 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -28,6 +28,6 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
 val mlexpr_of_ident : string -> MLast.expr
 
-val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr
+val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr
 
 val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index c35fa00d2e..8c85d01629 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -85,8 +85,9 @@ let make_fun_clauses loc s l =
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
   | ExtNonTerminal (nt, g, id) ->
+    let base s = <:expr< Pcoq.genarg_grammar $mk_extraarg loc s$ >> in
       <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
-      $mlexpr_of_prod_entry_key g$ >>
+      $mlexpr_of_prod_entry_key base g$ >>
 
 let mlexpr_of_clause cl =
   mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 3bb1e09076..d8c8850884 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -42,7 +42,7 @@ let rec make_let e = function
 
 let make_clause { r_patt = pt; r_branch = e; } =
   (make_patt pt,
-   vala (Some (make_when (MLast.loc_of_expr e) pt)),
+   vala None,
    make_let e pt)
 
 (* To avoid warnings *)
@@ -58,11 +58,11 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
   match c ,cg with
   | Some c, _ ->
      (make_patt pt,
-      vala (Some (make_when (MLast.loc_of_expr c) pt)),
+      vala None,
       make_let (mk_ignore c pt) pt)
   | None, Some cg ->
      (make_patt pt,
-      vala (Some (make_when (MLast.loc_of_expr cg) pt)),
+      vala None,
       <:expr< fun () -> $cg$ $str:s$ >>)
   | None, None -> msg_warning
       (strbrk("Vernac entry \""^s^"\" misses a classifier. "^
@@ -85,7 +85,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
        strbrk("Specific classifiers have precedence over global "^
          "classifiers. Only one classifier is called.")++fnl());
     (make_patt pt,
-      vala (Some (make_when loc pt)),
+      vala None,
       <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
 
 let make_fun_clauses loc s l =