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

The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.

After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.

24 files changed, 110 insertions, 23 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 57ae357dec..41e94914ee 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -23,12 +23,7 @@ let qualified_name loc s =
   let (name, path) = CList.sep_last path in
   qualified_name loc path name
 
-let mk_extraarg loc s =
-  try
-    let name = Genarg.get_name0 s in
-    qualified_name loc name
-  with Not_found ->
-    <:expr< $lid:"wit_"^s$ >>
+let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
   | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 1848bf85f1..3946d5d2b9 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -47,15 +47,6 @@ let mlexpr_of_option f = function
 let mlexpr_of_ident id =
   <:expr< Names.Id.of_string $str:id$ >>
 
-let repr_entry e =
-  let entry u =
-    let _ = Pcoq.get_entry u e in
-    Some (Entry.univ_name u, e)
-  in
-  try entry Pcoq.uprim with Not_found ->
-  try entry Pcoq.uconstr with Not_found ->
-  try entry Pcoq.utactic with Not_found -> None
-
 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$ >>
@@ -63,11 +54,7 @@ let rec mlexpr_of_prod_entry_key = function
   | 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 ->
-    begin match repr_entry e with
-    | None -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >>
-    | Some (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >>
-    end
+  | Extend.Uentry e -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >>
   | Extend.Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (CString.equal e "tactic");
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index ead4e39692..20ee7aa4fb 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -82,3 +82,13 @@ let () =
   register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
   register_name0 wit_bindings "Constrarg.wit_bindings";
   register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings";
+  ()
+
+(** Aliases *)
+
+let wit_reference = wit_ref
+let wit_global = wit_ref
+let wit_clause = wit_clause_dft_concl
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+let wit_redexpr = wit_red_expr
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 5c26af3c2a..1197b85a25 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -72,3 +72,15 @@ val wit_red_expr :
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
 
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_redexpr :
+  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 56b995e537..e497c996f7 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -28,3 +28,8 @@ let () = register_name0 wit_bool "Stdarg.wit_bool"
 let () = register_name0 wit_int "Stdarg.wit_int"
 let () = register_name0 wit_string "Stdarg.wit_string"
 let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident"
+
+(** Aliases for compatibility *)
+
+let wit_integer = wit_int
+let wit_preident = wit_pre_ident
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index d8904dab87..e1f648d7fc 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type
 val wit_string : string uniform_genarg_type
 
 val wit_pre_ident : string uniform_genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_integer : int uniform_genarg_type
+val wit_preident : string uniform_genarg_type
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 5dbc340caa..9a53e2e16a 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -9,6 +9,10 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Cctac
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 
 DECLARE PLUGIN "cc_plugin"
 
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 18570a6846..35a5a7616c 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index aec9586895..7bd07f6255 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -11,6 +11,10 @@
 (* ML names *)
 
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 open Pp
 open Names
 open Nameops
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 3e8be36993..587d10d1cc 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,6 +15,10 @@ open Goptions
 open Tacticals
 open Tacinterp
 open Libnames
+open Constrarg
+open Stdarg
+open Pcoq.Prim
+open Pcoq.Tactic
 
 DECLARE PLUGIN "ground_plugin"
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index dbcdeb83ad..4bd69b9fe7 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -16,8 +16,12 @@ open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
+open Constrarg
 open Tacticals
 open Misctypes
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "recdef_plugin"
 
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index bfc9c727d5..bca1c2febd 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -18,6 +18,10 @@
 
 open Errors
 open Misctypes
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Tactic
 
 DECLARE PLUGIN "micromega_plugin"
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 04c62eb487..b314e0d85f 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -19,6 +19,8 @@ DECLARE PLUGIN "omega_plugin"
 
 open Names
 open Coq_omega
+open Constrarg
+open Pcoq.Prim
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 7a3d7936a6..a15b0eb05a 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,6 +13,10 @@ open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "quote_plugin"
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 6b2b2bbfaf..61efa9f545 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -12,6 +12,8 @@ DECLARE PLUGIN "romega_plugin"
 
 open Names
 open Refl_omega
+open Constrarg
+open Pcoq.Prim
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 856ec0db5f..cd1d704dde 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -14,6 +14,11 @@ open Libnames
 open Printer
 open Newring_ast
 open Newring
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "newring_plugin"
 
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 7da6df717e..73b7bde9d7 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -13,6 +13,11 @@ open Names
 open Locus
 open Misctypes
 open Genredexpr
+open Stdarg
+open Constrarg
+open Pcoq.Constr
+open Pcoq.Prim
+open Pcoq.Tactic
 
 open Proofview.Notations
 open Sigma.Notations
@@ -143,7 +148,7 @@ END
 
 TACTIC EXTEND symmetry
   [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
-| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ]
+| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ]
 END
 
 (** Split *)
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 98868e8f91..8215e785ab 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -10,6 +10,10 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 open Names
 open Tacexpr
 open Taccoerce
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7df845e4bd..f7b379e69e 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -53,7 +53,6 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
-
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ae8b83b95e..52419497d1 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -10,7 +10,12 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
 open Extraargs
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 open Mod_subst
 open Names
 open Tacexpr
@@ -49,6 +54,8 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
+let clause = Pcoq.Tactic.clause_dft_concl
+
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
 -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4
index f4fae763fd..788443944f 100644
--- a/tactics/g_auto.ml4
+++ b/tactics/g_auto.ml4
@@ -10,6 +10,11 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 open Tacexpr
 
 DECLARE PLUGIN "g_auto"
@@ -128,7 +133,7 @@ TACTIC EXTEND dfs_eauto
 END
 
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) clause(cl) ] -> [ Eauto.autounfold_tac db cl ]
+| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ]
 END
 
 TACTIC EXTEND autounfold_one
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index 766593543c..9ef1545416 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -10,6 +10,11 @@
 
 open Misctypes
 open Class_tactics
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
+open Stdarg
+open Constrarg
 
 DECLARE PLUGIN "g_class"
 
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 0ce886373f..c4ef1f297e 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -20,6 +20,11 @@ open Extraargs
 open Tacmach
 open Tacticals
 open Rewrite
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "g_rewrite"
 
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 2a5676525a..dd11efebd8 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -16,6 +16,12 @@
 open Libnames
 open Constrexpr
 open Constrexpr_ops
+open Stdarg
+open Constrarg
+open Extraargs
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 (* We define new entries for programs, with the use of this module
  * Subtac. These entries are named Subtac.<foo>