Moving Ltac-specific parsing API to ltac/ folder.

22 files changed, 145 insertions, 117 deletions

diff --git a/dev/base_include b/dev/base_include
index b09b6df2d..0abcefc38 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Pcoq.Tactic.tactic;;
+let parse_tac    = Pcoq.parse_string Pltac.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 2d5c40894..919ca3ad7 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -70,8 +70,8 @@ let rec mlexpr_of_prod_entry_key f = function
   | Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (e = "tactic");
-    if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >>
-    else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
+    if l = 5 then <:expr< Extend.Aentry (Pltac.binder_tactic) >>
+    else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >>
 
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index c6d72e03e..c32f757d9 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -35,11 +35,11 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Constrarg.wit_ident
 let () = create_generic_quotation "reference" Pcoq.Prim.reference Constrarg.wit_ref
 let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr
 let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr
-let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern
+let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Constrarg.wit_intro_pattern
 let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
-  Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+  Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5)
 
 (** Backward-compatible tactic notation entry names *)
 
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index be8390c95..d16ed84a2 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -14,7 +14,7 @@ open Stdarg
 open Constrarg
 open Extraargs
 open Pcoq.Prim
-open Pcoq.Tactic
+open Pltac
 open Mod_subst
 open Names
 open Tacexpr
@@ -53,7 +53,7 @@ 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
+let clause = Pltac.clause_dft_concl
 
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 8bc2ffd65..eb1dc9081 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -14,7 +14,7 @@ open Stdarg
 open Constrarg
 open Pcoq.Prim
 open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
 open Tacexpr
 
 DECLARE PLUGIN "g_auto"
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index eaa6aad4f..3cdb3a6c7 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -10,7 +10,7 @@
 
 open Misctypes
 open Class_tactics
-open Pcoq.Tactic
+open Pltac
 open Stdarg
 open Constrarg
 
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 788ba3b8e..f17cbc9a3 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -22,7 +22,7 @@ open Pcoq
 open Pcoq.Constr
 open Pcoq.Vernac_
 open Pcoq.Prim
-open Pcoq.Tactic
+open Pltac
 
 let fail_default_value = ArgArg 0
 
@@ -334,20 +334,20 @@ GEXTEND Gram
     [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ]
   ;
   command:
-    [ [ IDENT "Proof"; "with"; ta = Pcoq.Tactic.tactic; 
+    [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; 
         l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
           Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l)
       | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
-        ta = OPT [ "with"; ta = Pcoq.Tactic.tactic -> in_tac ta ] ->
+        ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] ->
           Vernacexpr.VernacProof (ta,Some l) ] ]
   ;
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
-        tac = Pcoq.Tactic.tactic ->
+        tac = Pltac.tactic ->
           Vernacexpr.HintsExtern (n,c, in_tac tac) ] ]
   ;
   operconstr: LEVEL "0"
-    [ [ IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" ->
+    [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
           let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in
           CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
   ;
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index db8daf32d..df0b3e855 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -46,7 +46,7 @@ let with_tac f tac =
  *)
 
 module Gram = Pcoq.Gram
-module Tactic = Pcoq.Tactic
+module Tactic = Pltac
 
 open Pcoq
 
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 82b79c883..cdcbfdb7c 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -22,9 +22,10 @@ open Tacticals
 open Rewrite
 open Stdarg
 open Constrarg
+open Pcoq.Vernac_
 open Pcoq.Prim
 open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
 
 DECLARE PLUGIN "g_rewrite"
 
diff --git a/parsing/g_tactic.ml4 b/ltac/g_tactic.ml4
index 3c2c45c72..4e657fe83 100644
--- a/parsing/g_tactic.ml4
+++ b/ltac/g_tactic.ml4
@@ -120,7 +120,7 @@ let lookup_at_as_comma =
 
 open Constr
 open Prim
-open Tactic
+open Pltac
 
 let mk_fix_tac (loc,id,bl,ann,ty) =
   let n =
@@ -217,6 +217,8 @@ let warn_deprecated_eqn_syntax =
 
 (* Auxiliary grammar rules *)
 
+open Vernac_
+
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
   bindings red_expr int_or_var open_constr uconstr
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index fc51e48ae..1fe29b115 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -1,3 +1,4 @@
+Pltac
 Taccoerce
 Tacsubst
 Tacenv
@@ -19,4 +20,5 @@ Rewrite
 G_rewrite
 Tauto
 G_eqdecide
+G_tactic
 G_ltac
diff --git a/ltac/pltac.ml b/ltac/pltac.ml
new file mode 100644
index 000000000..148867aac
--- /dev/null
+++ b/ltac/pltac.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Pcoq
+
+(* Main entry for extensions *)
+let simple_tactic = Gram.entry_create "tactic:simple_tactic"
+
+let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name)
+
+(* Entries that can be referred via the string -> Gram.entry table *)
+(* Typically for tactic user extensions *)
+let open_constr =
+  make_gen_entry utactic "open_constr"
+let constr_with_bindings =
+  make_gen_entry utactic "constr_with_bindings"
+let bindings =
+  make_gen_entry utactic "bindings"
+let hypident = Gram.entry_create "hypident"
+let constr_may_eval = make_gen_entry utactic "constr_may_eval"
+let constr_eval = make_gen_entry utactic "constr_eval"
+let uconstr =
+  make_gen_entry utactic "uconstr"
+let quantified_hypothesis =
+  make_gen_entry utactic "quantified_hypothesis"
+let destruction_arg = make_gen_entry utactic "destruction_arg"
+let int_or_var = make_gen_entry utactic "int_or_var"
+let simple_intropattern =
+  make_gen_entry utactic "simple_intropattern"
+let clause_dft_concl = 
+  make_gen_entry utactic "clause"
+
+
+(* Main entries for ltac *)
+let tactic_arg = Gram.entry_create "tactic:tactic_arg"
+let tactic_expr = make_gen_entry utactic "tactic_expr"
+let binder_tactic = make_gen_entry utactic "binder_tactic"
+
+let tactic = make_gen_entry utactic "tactic"
+
+(* Main entry for quotations *)
+let tactic_eoi = eoi_entry tactic
+
+let () =
+  let open Stdarg in
+  let open Constrarg in
+  register_grammar wit_int_or_var (int_or_var);
+  register_grammar wit_intro_pattern (simple_intropattern);
+  register_grammar wit_quant_hyp (quantified_hypothesis);
+  register_grammar wit_uconstr (uconstr);
+  register_grammar wit_open_constr (open_constr);
+  register_grammar wit_constr_with_bindings (constr_with_bindings);
+  register_grammar wit_bindings (bindings);
+  register_grammar wit_tactic (tactic);
+  register_grammar wit_ltac (tactic);
+  register_grammar wit_clause_dft_concl (clause_dft_concl);
+  register_grammar wit_destruction_arg (destruction_arg);
+  ()
diff --git a/ltac/pltac.mli b/ltac/pltac.mli
new file mode 100644
index 000000000..27eb9f280
--- /dev/null
+++ b/ltac/pltac.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Ltac parsing entries *)
+
+open Loc
+open Names
+open Pcoq
+open Libnames
+open Constrexpr
+open Tacexpr
+open Genredexpr
+open Misctypes
+
+val open_constr : constr_expr Gram.entry
+val constr_with_bindings : constr_expr with_bindings Gram.entry
+val bindings : constr_expr bindings Gram.entry
+val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
+val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
+val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
+val uconstr : constr_expr Gram.entry
+val quantified_hypothesis : quantified_hypothesis Gram.entry
+val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
+val int_or_var : int or_var Gram.entry
+val simple_tactic : raw_tactic_expr Gram.entry
+val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
+val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
+val tactic_arg : raw_tactic_arg Gram.entry
+val tactic_expr : raw_tactic_expr Gram.entry
+val binder_tactic : raw_tactic_expr Gram.entry
+val tactic : raw_tactic_expr Gram.entry
+val tactic_eoi : raw_tactic_expr Gram.entry
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index d05beb392..fcdb1875d 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -43,8 +43,8 @@ let coincide s pat off =
   !break
 
 let atactic n =
-  if n = 5 then Aentry Tactic.binder_tactic
-  else Aentryl (Tactic.tactic_expr, n)
+  if n = 5 then Aentry Pltac.binder_tactic
+  else Aentryl (Pltac.tactic_expr, n)
 
 type entry_name = EntryName :
   'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
@@ -108,11 +108,11 @@ let interp_entry_name interp symb =
 
 let get_tactic_entry n =
   if Int.equal n 0 then
-    Tactic.simple_tactic, None
+    Pltac.simple_tactic, None
   else if Int.equal n 5 then
-    Tactic.binder_tactic, None
+    Pltac.binder_tactic, None
   else if 1<=n && n<5 then
-    Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
+    Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
   else
     error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
 
@@ -405,7 +405,7 @@ let create_ltac_quotation name cast (e, l) =
   in
   let action _ v _ _ _ loc = cast (loc, v) in
   let gram = (level, assoc, [Rule (rule, action)]) in
-  Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
+  Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
 
 (** Command *)
 
@@ -434,7 +434,7 @@ let register_ltac local tacl =
         in
         let is_shadowed =
           try
-            match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
+            match Pcoq.parse_string Pltac.tactic (Id.to_string id) with
             | Tacexpr.TacArg _ -> false
             | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
           with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
@@ -517,9 +517,9 @@ let print_ltacs () =
 let () =
   let open Metasyntax in
   let entries = [
-    AnyEntry Pcoq.Tactic.tactic_expr;
-    AnyEntry Pcoq.Tactic.binder_tactic;
-    AnyEntry Pcoq.Tactic.simple_tactic;
-    AnyEntry Pcoq.Tactic.tactic_arg;
+    AnyEntry Pltac.tactic_expr;
+    AnyEntry Pltac.binder_tactic;
+    AnyEntry Pltac.simple_tactic;
+    AnyEntry Pltac.tactic_arg;
   ] in
   register_grammar "tactic" entries
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7cb897cf7..51c4733aa 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -260,7 +260,7 @@ GEXTEND Gram
         ProveBody (bl, t) ] ]
   ;
   reduce:
-    [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
+    [ [ IDENT "Eval"; r = red_expr; "in" -> Some r
       | -> None ] ]
   ;
   one_decl_notation:
@@ -867,7 +867,7 @@ GEXTEND Gram
 	  VernacRemoveOption ([table], v) ]] 
   ;
   query_command: (* TODO: rapprocher Eval et Check *)
-    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
+    [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr ->
           fun g -> VernacCheckMayEval (Some r, g, c)
       | IDENT "Compute"; c = lconstr ->
 	  fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c)
@@ -1024,7 +1024,7 @@ GEXTEND Gram
 (* registration of a custom reduction *)
 
       | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":=";
-         r = Tactic.red_expr ->
+         r = red_expr ->
 	   VernacDeclareReduction (s,r)
 
  ] ];
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index 8df519b56..05e2911c2 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -2,4 +2,3 @@ G_constr
 G_vernac
 G_prim
 G_proofs
-G_tactic
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 714e25f85..e3a66dc11 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -324,47 +324,6 @@ module Module =
     let module_type = Gram.entry_create "module_type"
   end
 
-module Tactic =
-  struct
-    (* Main entry for extensions *)
-    let simple_tactic = Gram.entry_create "tactic:simple_tactic"
-
-    (* Entries that can be referred via the string -> Gram.entry table *)
-    (* Typically for tactic user extensions *)
-    let open_constr =
-      make_gen_entry utactic "open_constr"
-    let constr_with_bindings =
-      make_gen_entry utactic "constr_with_bindings"
-    let bindings =
-      make_gen_entry utactic "bindings"
-    let hypident = Gram.entry_create "hypident"
-    let constr_may_eval = make_gen_entry utactic "constr_may_eval"
-    let constr_eval = make_gen_entry utactic "constr_eval"
-    let uconstr =
-      make_gen_entry utactic "uconstr"
-    let quantified_hypothesis =
-      make_gen_entry utactic "quantified_hypothesis"
-    let destruction_arg = make_gen_entry utactic "destruction_arg"
-    let int_or_var = make_gen_entry utactic "int_or_var"
-    let red_expr = make_gen_entry utactic "red_expr"
-    let simple_intropattern =
-      make_gen_entry utactic "simple_intropattern"
-    let clause_dft_concl = 
-      make_gen_entry utactic "clause"
-
-
-    (* Main entries for ltac *)
-    let tactic_arg = Gram.entry_create "tactic:tactic_arg"
-    let tactic_expr = make_gen_entry utactic "tactic_expr"
-    let binder_tactic = make_gen_entry utactic "binder_tactic"
-
-    let tactic = make_gen_entry utactic "tactic"
-
-    (* Main entry for quotations *)
-    let tactic_eoi = eoi_entry tactic
-
-  end
-
 module Vernac_ =
   struct
     let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
@@ -377,6 +336,7 @@ module Vernac_ =
     let vernac = gec_vernac "Vernac.vernac"
     let vernac_eoi = eoi_entry vernac
     let rec_definition = gec_vernac "Vernac.rec_definition"
+    let red_expr = make_gen_entry utactic "red_expr"
     (* Main vernac entry *)
     let main_entry = Gram.entry_create "vernac"
     let noedit_mode = gec_vernac "noedit_command"
@@ -499,26 +459,12 @@ let with_grammar_rule_protection f x =
 let () =
   let open Stdarg in
   let open Constrarg in
-(*   Grammar.register0 wit_unit; *)
-(*   Grammar.register0 wit_bool; *)
   Grammar.register0 wit_int (Prim.integer);
   Grammar.register0 wit_string (Prim.string);
   Grammar.register0 wit_pre_ident (Prim.preident);
-  Grammar.register0 wit_int_or_var (Tactic.int_or_var);
-  Grammar.register0 wit_intro_pattern (Tactic.simple_intropattern);
   Grammar.register0 wit_ident (Prim.ident);
   Grammar.register0 wit_var (Prim.var);
   Grammar.register0 wit_ref (Prim.reference);
-  Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis);
   Grammar.register0 wit_constr (Constr.constr);
-  Grammar.register0 wit_uconstr (Tactic.uconstr);
-  Grammar.register0 wit_open_constr (Tactic.open_constr);
-  Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings);
-  Grammar.register0 wit_bindings (Tactic.bindings);
-(*   Grammar.register0 wit_hyp_location_flag; *)
-  Grammar.register0 wit_red_expr (Tactic.red_expr);
-  Grammar.register0 wit_tactic (Tactic.tactic);
-  Grammar.register0 wit_ltac (Tactic.tactic);
-  Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl);
-  Grammar.register0 wit_destruction_arg (Tactic.destruction_arg);
+  Grammar.register0 wit_red_expr (Vernac_.red_expr);
   ()
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 635b0170a..82ec49417 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -12,7 +12,6 @@ open Extend
 open Vernacexpr
 open Genarg
 open Constrexpr
-open Tacexpr
 open Libnames
 open Misctypes
 open Genredexpr
@@ -177,29 +176,6 @@ module Module :
     val module_type : module_ast Gram.entry
   end
 
-module Tactic :
-  sig
-    val open_constr : constr_expr Gram.entry
-    val constr_with_bindings : constr_expr with_bindings Gram.entry
-    val bindings : constr_expr bindings Gram.entry
-    val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
-    val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
-    val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
-    val uconstr : constr_expr Gram.entry
-    val quantified_hypothesis : quantified_hypothesis Gram.entry
-    val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
-    val int_or_var : int or_var Gram.entry
-    val red_expr : raw_red_expr Gram.entry
-    val simple_tactic : raw_tactic_expr Gram.entry
-    val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
-    val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
-    val tactic_arg : raw_tactic_arg Gram.entry
-    val tactic_expr : raw_tactic_expr Gram.entry
-    val binder_tactic : raw_tactic_expr Gram.entry
-    val tactic : raw_tactic_expr Gram.entry
-    val tactic_eoi : raw_tactic_expr Gram.entry
-  end
-
 module Vernac_ :
   sig
     val gallina : vernac_expr Gram.entry
@@ -211,6 +187,7 @@ module Vernac_ :
     val vernac_eoi : vernac_expr Gram.entry
     val noedit_mode : vernac_expr Gram.entry
     val command_entry : vernac_expr Gram.entry
+    val red_expr : raw_red_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 6c17dcc4f..18a35c6cf 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -19,7 +19,7 @@ open Vernacexpr
 open Tok (* necessary for camlp4 *)
 
 open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
 open Ppdecl_proof
 
 let pr_goal gs =
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 42e490315..6368c2536 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -18,7 +18,7 @@ open Constrarg
 open Misctypes
 open Pcoq.Prim
 open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
 
 DECLARE PLUGIN "recdef_plugin"
 
@@ -143,7 +143,7 @@ END
 
 module Gram = Pcoq.Gram
 module Vernac = Pcoq.Vernac_
-module Tactic = Pcoq.Tactic
+module Tactic = Pltac
 
 type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
 
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 216eb8b37..1a0020031 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -17,7 +17,7 @@ open Newring
 open Stdarg
 open Constrarg
 open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
 
 DECLARE PLUGIN "newring_plugin"
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 5fb0bb664..150be9d72 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -41,7 +41,7 @@ open Proofview.Notations
 open Tacinterp
 open Pretyping
 open Constr
-open Tactic
+open Pltac
 open Extraargs
 open Ppconstr
 open Printer