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.

7 files changed, 33 insertions, 3 deletions

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"