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 57ae357de..41e94914e 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 1848bf85f..3946d5d2b 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 ead4e3969..20ee7aa4f 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 5c26af3c2..1197b85a2 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 56b995e53..e497c996f 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 d8904dab8..e1f648d7f 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 5dbc340ca..9a53e2e16 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 18570a684..35a5a7616 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 aec958689..7bd07f625 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 3e8be3699..587d10d1c 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 dbcdeb83a..4bd69b9fe 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 bfc9c727d..bca1c2feb 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 04c62eb48..b314e0d85 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 7a3d7936a..a15b0eb05 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 6b2b2bbfa..61efa9f54 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 856ec0db5..cd1d704dd 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 7da6df717..73b7bde9d 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 98868e8f9..8215e785a 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 7df845e4b..f7b379e69 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 ae8b83b95..52419497d 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 f4fae763f..788443944 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 766593543..9ef154541 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 0ce886373..c4ef1f297 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 2a5676525..dd11efebd 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>