Merge PR #7558: [api] Make `vernac/` self-contained.

35 files changed, 225 insertions, 126 deletions

diff --git a/META.coq b/META.coq
index 8d4c3d5f0..cdc088e74 100644
--- a/META.coq
+++ b/META.coq
@@ -6,6 +6,18 @@ version = "8.8"
 directory = ""
 requires = "camlp5"
 
+package "grammar" (
+
+  description = "Coq Camlp5 Grammar Extensions for Plugins"
+  version     = "8.8"
+
+  requires    = "camlp5.gramlib"
+  directory   = "grammar"
+
+  archive(byte)   = "grammar.cma"
+  archive(native) = "grammar.cmxa"
+)
+
 package "config" (
 
   description = "Coq Configuration Variables"
@@ -126,18 +138,6 @@ package "interp" (
 
 )
 
-package "grammar" (
-
-  description = "Coq Camlp5 Grammar Extensions for Plugins"
-  version     = "8.8"
-
-  requires    = "camlp5.gramlib"
-  directory   = "grammar"
-
-  archive(byte)   = "grammar.cma"
-  archive(native) = "grammar.cmxa"
-)
-
 package "proofs" (
 
   description = "Coq Proof Engine"
diff --git a/dev/base_include b/dev/base_include
index 8d81ca3e0..fc38305cc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -189,7 +189,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
+let parse_vernac = Pcoq.parse_string Pvernac.Vernac_.vernac_control;;
 let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
new file mode 100644
index 000000000..115f29f1e
--- /dev/null
+++ b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
@@ -0,0 +1,14 @@
+if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then
+
+    _OVERLAY_BRANCH=vernac+move_parser
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    ltac2_CI_BRANCH="$_OVERLAY_BRANCH"
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index cd28b1b50..346b7c7dd 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -4,7 +4,7 @@
 
 Misctypes
 
-  Syntax for universe sorts and kinds has been moved from `Misctypes`
+- Syntax for universe sorts and kinds has been moved from `Misctypes`
   to `Glob_term`, as these are turned into kernel terms by
   `Pretyping`.
 
@@ -41,6 +41,16 @@ Printer.ml API
   pr_subgoal and pr_goal was removed to simplify the code.  It was
   earlierly used by PCoq.
 
+Vernacular commands
+
+- The implementation of vernacular commands has been refactored so it
+  is self-contained now, including the parsing and extension
+  mechanisms. This involves a couple of non-backward compatible
+  changes due to layering issues, where some functions have been moved
+  from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in
+  `tactics/`. In all cases adapting is a matter of changing the module
+  name.
+
 ### Unit testing
 
   The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 103e1188a..da4a0421b 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,11 +1,6 @@
 Tok
 CLexer
 Extend
-Vernacexpr
 Pcoq
-Egramml
-Egramcoq
 G_constr
-G_vernac
 G_prim
-G_proofs
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 258c4bb11..b78c35c26 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -145,7 +145,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
 
 end
 
-
 let warning_verbose = Gramext.warning_verbose
 
 let of_coq_assoc = function
@@ -387,7 +386,6 @@ let create_universe u =
 let uprim   = create_universe "prim"
 let uconstr = create_universe "constr"
 let utactic = create_universe "tactic"
-let uvernac = create_universe "vernac"
 
 let get_univ u =
   if Hashtbl.mem utables u then u
@@ -493,44 +491,6 @@ module Module =
     let module_type = Gram.entry_create "module_type"
   end
 
-module Vernac_ =
-  struct
-    let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
-
-    (* The different kinds of vernacular commands *)
-    let gallina = gec_vernac "gallina"
-    let gallina_ext = gec_vernac "gallina_ext"
-    let command = gec_vernac "command"
-    let syntax = gec_vernac "syntax_command"
-    let vernac_control = gec_vernac "Vernac.vernac_control"
-    let rec_definition = gec_vernac "Vernac.rec_definition"
-    let red_expr = make_gen_entry utactic "red_expr"
-    let hint_info = gec_vernac "hint_info"
-    (* Main vernac entry *)
-    let main_entry = Gram.entry_create "vernac"
-    let noedit_mode = gec_vernac "noedit_command"
-
-    let () =
-      let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in
-      let act_eoi = Gram.action (fun _ loc -> None) in
-      let rule = [
-        ([ Symbols.stoken Tok.EOI ], act_eoi);
-        ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
-      ] in
-      uncurry (Gram.extend main_entry) (None, make_rule rule)
-
-    let command_entry_ref = ref noedit_mode
-    let command_entry =
-      Gram.Entry.of_parser "command_entry"
-        (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
-
-  end
-
-let main_entry = Vernac_.main_entry
-
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
-
 let epsilon_value f e =
   let r = Rule (Next (Stop, e), fun x _ -> f x) in
   let ext = of_coq_extend_statement (None, [None, None, [r]]) in
@@ -635,7 +595,6 @@ let () =
   Grammar.register0 wit_ref (Prim.reference);
   Grammar.register0 wit_sort_family (Constr.sort_family);
   Grammar.register0 wit_constr (Constr.constr);
-  Grammar.register0 wit_red_expr (Vernac_.red_expr);
   ()
 
 (** Registering extra grammar *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 387a62604..36e5e420a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -10,12 +10,10 @@
 
 open Names
 open Extend
-open Vernacexpr
 open Genarg
 open Constrexpr
 open Libnames
 open Misctypes
-open Genredexpr
 
 (** The parser of Coq *)
 
@@ -89,6 +87,12 @@ module type S =
 
 end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
 
+module Symbols : sig
+
+  val stoken : Tok.t -> Gram.symbol
+  val snterm : Gram.internal_entry -> Gram.symbol
+end
+
 (** The parser of Coq is built from three kinds of rule declarations:
 
    - dynamic rules declared at the evaluation of Coq files (using
@@ -177,11 +181,14 @@ val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
 type gram_universe
 
 val get_univ : string -> gram_universe
+val create_universe : string -> gram_universe
+
+val new_entry : gram_universe -> string -> 'a Gram.entry
 
 val uprim : gram_universe
 val uconstr : gram_universe
 val utactic : gram_universe
-val uvernac : gram_universe
+
 
 val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
 val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
@@ -249,27 +256,6 @@ module Module :
     val module_type : module_ast Gram.entry
   end
 
-module Vernac_ :
-  sig
-    val gallina : vernac_expr Gram.entry
-    val gallina_ext : vernac_expr Gram.entry
-    val command : vernac_expr Gram.entry
-    val syntax : vernac_expr Gram.entry
-    val vernac_control : vernac_control Gram.entry
-    val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
-    val noedit_mode : vernac_expr Gram.entry
-    val command_entry : vernac_expr Gram.entry
-    val red_expr : raw_red_expr Gram.entry
-    val hint_info : Typeclasses.hint_info_expr Gram.entry
-  end
-
-(** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Gram.entry
-
-(** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Gram.entry
-val set_command_entry : vernac_expr Gram.entry -> unit
-
 val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** {5 Extending the parser without synchronization} *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d193e1144..0a2741ad1 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -125,7 +125,7 @@ ARGUMENT EXTEND auto_using'
 END
 
 module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
+module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
 
 type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index c21921513..17011f206 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -320,7 +320,7 @@ let project_hint ~poly pri l2r r =
 
 let add_hints_iff ~atts l2r lc n bl =
   let open Vernacinterp in
-  Hints.add_hints (Locality.make_module_locality atts.locality) bl
+  Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl
     (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
 
 VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 643f7e99f..07047d016 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -219,7 +219,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
     fun ~atts ~st -> begin
         let open Vernacinterp in
         let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
-        Hints.add_hints (Locality.make_section_locality atts.locality)
+        Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
           (match dbnames with None -> ["core"] | Some l -> l) entry;
         st
       end
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 4857beffa..ed54320a5 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -21,9 +21,9 @@ open Tok (* necessary for camlp5 *)
 open Names
 
 open Pcoq
-open Pcoq.Constr
-open Pcoq.Vernac_
 open Pcoq.Prim
+open Pcoq.Constr
+open Pvernac.Vernac_
 open Pltac
 
 let fail_default_value = ArgArg 0
@@ -58,8 +58,8 @@ let tacdef_body = new_entry "tactic:tacdef_body"
 let _ =
   let mode = {
     Proof_global.name = "Classic";
-    set = (fun () -> set_command_entry tactic_mode);
-    reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+    set = (fun () -> Pvernac.set_command_entry tactic_mode);
+    reset = (fun () -> Pvernac.(set_command_entry noedit_mode));
   } in
   Proof_global.register_proof_mode mode
 
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fbaa2e58f..079001ee4 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -20,9 +20,9 @@ open Extraargs
 open Tacmach
 open Rewrite
 open Stdarg
-open Pcoq.Vernac_
 open Pcoq.Prim
 open Pcoq.Constr
+open Pvernac.Vernac_
 open Pltac
 
 DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 7534e2799..dc9f607cf 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -211,7 +211,7 @@ let warn_deprecated_eqn_syntax =
 
 (* Auxiliary grammar rules *)
 
-open Vernac_
+open Pvernac.Vernac_
 
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 7ac9ea89d..750461a1b 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -19,7 +19,7 @@ open Constrexpr_ops
 open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
-open Pcoq.Vernac_
+open Pvernac.Vernac_
 open Ltac_plugin
 open Notation_ops
 open Notation_term
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 86b68d8fb..b69d8a9ef 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -4,4 +4,3 @@ Ppconstr
 Printer
 Printmod
 Prettyp
-Ppvernac
diff --git a/stm/stm.ml b/stm/stm.ml
index b8fe8ddd7..c394be22e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2976,7 +2976,7 @@ let parse_sentence ~doc sid pa =
        str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
   Flags.with_option Flags.we_are_parsing (fun () ->
       try
-        match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+        match Pcoq.Gram.entry_parse Pvernac.main_entry pa with
         | None            -> raise End_of_input
         | Some (loc, cmd) -> CAst.make ~loc cmd
       with e when CErrors.noncritical e ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 786760122..7b5be4c1c 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -28,7 +28,6 @@ open Termops
 open Inductiveops
 open Typing
 open Decl_kinds
-open Vernacexpr
 open Typeclasses
 open Pattern
 open Patternops
@@ -156,6 +155,24 @@ type full_hint = hint with_metadata
 type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
 
+type reference_or_constr =
+  | HintsReference of reference
+  | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+  | ModeInput (* No evars *)
+  | ModeNoHeadEvar (* No evar at the head *)
+  | ModeOutput (* Anything *)
+
+type hints_expr =
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of reference list
+  | HintsTransparency of reference list * bool
+  | HintsMode of reference * hint_mode list
+  | HintsConstructors of reference list
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
 type import_level = [ `LAX | `WARN | `STRICT ]
 
 let warn_hint : import_level ref = ref `LAX
@@ -1326,7 +1343,7 @@ let interp_hints poly =
       let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
-let add_hints local dbnames0 h =
+let add_hints ~local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
     user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
   let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index c7de10a2a..f05988703 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -18,7 +18,6 @@ open Misctypes
 open Tactypes
 open Clenv
 open Pattern
-open Vernacexpr
 
 (** {6 General functions. } *)
 
@@ -71,6 +70,24 @@ type search_entry
 
 type hint_entry
 
+type reference_or_constr =
+  | HintsReference of Libnames.reference
+  | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+  | ModeInput (* No evars *)
+  | ModeNoHeadEvar (* No evar at the head *)
+  | ModeOutput (* Anything *)
+
+type hints_expr =
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of Libnames.reference list
+  | HintsTransparency of Libnames.reference list * bool
+  | HintsMode of Libnames.reference * hint_mode list
+  | HintsConstructors of Libnames.reference list
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
 type 'a hints_path_gen =
   | PathAtom of 'a hints_path_atom_gen
   | PathStar of 'a hints_path_gen
@@ -178,7 +195,7 @@ val current_pure_db : unit -> hint_db list
 
 val interp_hints : polymorphic -> hints_expr -> hints_entry
 
-val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
+val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.ml4
index d5d558b9b..e3cefe236 100644
--- a/toplevel/g_toplevel.ml4
+++ b/toplevel/g_toplevel.ml4
@@ -35,7 +35,7 @@ GEXTEND Gram
       | IDENT "Quit"; "." -> CAst.make VernacQuit
       | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
         CAst.make (VernacBacktrack (n,m,p))
-      | cmd = main_entry ->
+      | cmd = Pvernac.main_entry ->
               match cmd with
               | None -> raise Stm.End_of_input
               | Some (loc,c) -> CAst.make ~loc (VernacControl c)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d99d45313..40001c0a3 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -41,7 +41,7 @@ let _ = Goptions.declare_bool_option {
 let typeclasses_db = "typeclass_instances"
 
 let set_typeclass_transparency c local b = 
-  Hints.add_hints local [typeclasses_db] 
+  Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry ([c], b))
     
 let _ =
@@ -56,7 +56,7 @@ let _ =
                      (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
 		     info.hint_pattern } in
      Flags.silently (fun () ->
-	Hints.add_hints local [typeclasses_db]
+       Hints.add_hints ~local [typeclasses_db]
 	  (Hints.HintsResolveEntry
 	     [info, poly, false, Hints.PathHints path, inst'])) ());
   Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
diff --git a/parsing/egramcoq.ml b/vernac/egramcoq.ml
index 5f63d21c4..5f63d21c4 100644
--- a/parsing/egramcoq.ml
+++ b/vernac/egramcoq.ml
diff --git a/parsing/egramcoq.mli b/vernac/egramcoq.mli
index e15add10f..e15add10f 100644
--- a/parsing/egramcoq.mli
+++ b/vernac/egramcoq.mli
diff --git a/parsing/egramml.ml b/vernac/egramml.ml
index 90cd7d10b..048d4d93a 100644
--- a/parsing/egramml.ml
+++ b/vernac/egramml.ml
@@ -77,7 +77,7 @@ let get_extend_vernac_rule (s, i) =
   | Failure _ -> raise Not_found
 
 let extend_vernac_command_grammar s nt gl =
-  let nt = Option.default Vernac_.command nt in
+  let nt = Option.default Pvernac.Vernac_.command nt in
   vernac_exts := (s,gl) :: !vernac_exts;
   let mkact loc l = VernacExtend (s, l) in
   let rules = [make_rule mkact gl] in
diff --git a/parsing/egramml.mli b/vernac/egramml.mli
index 31aa1a989..31aa1a989 100644
--- a/parsing/egramml.mli
+++ b/vernac/egramml.mli
diff --git a/parsing/g_proofs.ml4 b/vernac/g_proofs.ml4
index 4f3d83a8a..56229c765 100644
--- a/parsing/g_proofs.ml4
+++ b/vernac/g_proofs.ml4
@@ -16,7 +16,7 @@ open Misctypes
 open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
-open Pcoq.Vernac_
+open Pvernac.Vernac_
 
 let thm_token = G_vernac.thm_token
 
diff --git a/parsing/g_vernac.ml4 b/vernac/g_vernac.ml4
index a1c563f53..6c7df8cfa 100644
--- a/parsing/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -25,8 +25,8 @@ open Tok (* necessary for camlp5 *)
 open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
-open Pcoq.Vernac_
 open Pcoq.Module
+open Pvernac.Vernac_
 
 let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
 let _ = List.iter CLexer.add_keyword vernac_kw
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 76958b05f..e038f54dd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -76,15 +76,15 @@ let pr_grammar = function
       pr_entry Pcoq.Constr.pattern
   | "vernac" ->
       str "Entry vernac_control is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.vernac_control ++
+      pr_entry Pvernac.Vernac_.vernac_control ++
       str "Entry command is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.command ++
+      pr_entry Pvernac.Vernac_.command ++
       str "Entry syntax is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.syntax ++
+      pr_entry Pvernac.Vernac_.syntax ++
       str "Entry gallina is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.gallina ++
+      pr_entry Pvernac.Vernac_.gallina ++
       str "Entry gallina_ext is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.gallina_ext
+      pr_entry Pvernac.Vernac_.gallina_ext
   | name -> pr_registered_grammar name
 
 (**********************************************************************)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index dfc51a990..6ef8294df 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -616,7 +616,7 @@ let shrink_body c ty =
 let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
 let add_hint local prg cst =
-  Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+  Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
 
 let it_mkLambda_or_LetIn_or_clean t ctx =
   let open Context.Rel.Declaration in
diff --git a/printing/ppvernac.ml b/vernac/ppvernac.ml
index 7a34e8027..3655947a5 100644
--- a/printing/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -152,7 +152,7 @@ open Pputils
       | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
       | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
       | SearchAbout sl ->
-	 keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
+         keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
   let pr_locality local = if local then keyword "Local" else keyword "Global"
 
diff --git a/printing/ppvernac.mli b/vernac/ppvernac.mli
index 4aa24bf5d..4aa24bf5d 100644
--- a/printing/ppvernac.mli
+++ b/vernac/ppvernac.mli
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
new file mode 100644
index 000000000..bac882381
--- /dev/null
+++ b/vernac/pvernac.ml
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pcoq
+
+let uncurry f (x,y) = f x y
+
+let uvernac = create_universe "vernac"
+
+module Vernac_ =
+  struct
+    let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
+
+    (* The different kinds of vernacular commands *)
+    let gallina = gec_vernac "gallina"
+    let gallina_ext = gec_vernac "gallina_ext"
+    let command = gec_vernac "command"
+    let syntax = gec_vernac "syntax_command"
+    let vernac_control = gec_vernac "Vernac.vernac_control"
+    let rec_definition = gec_vernac "Vernac.rec_definition"
+    let red_expr = new_entry utactic "red_expr"
+    let hint_info = gec_vernac "hint_info"
+    (* Main vernac entry *)
+    let main_entry = Gram.entry_create "vernac"
+    let noedit_mode = gec_vernac "noedit_command"
+
+    let () =
+      let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in
+      let act_eoi = Gram.action (fun _ loc -> None) in
+      let rule = [
+        ([ Symbols.stoken Tok.EOI ], act_eoi);
+        ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
+      ] in
+      uncurry (Gram.extend main_entry) (None, [None, None, rule])
+
+    let command_entry_ref = ref noedit_mode
+    let command_entry =
+      Gram.Entry.of_parser "command_entry"
+        (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
+
+  end
+
+let main_entry = Vernac_.main_entry
+
+let set_command_entry e = Vernac_.command_entry_ref := e
+let get_command_entry () = !Vernac_.command_entry_ref
+
+let () =
+  register_grammar Stdarg.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
new file mode 100644
index 000000000..9d999793e
--- /dev/null
+++ b/vernac/pvernac.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pcoq
+open Genredexpr
+open Vernacexpr
+
+val uvernac : gram_universe
+
+module Vernac_ :
+  sig
+    val gallina : vernac_expr Gram.entry
+    val gallina_ext : vernac_expr Gram.entry
+    val command : vernac_expr Gram.entry
+    val syntax : vernac_expr Gram.entry
+    val vernac_control : vernac_control Gram.entry
+    val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
+    val noedit_mode : vernac_expr Gram.entry
+    val command_entry : vernac_expr Gram.entry
+    val red_expr : raw_red_expr Gram.entry
+    val hint_info : Typeclasses.hint_info_expr Gram.entry
+  end
+
+(** The main entry: reads an optional vernac command *)
+val main_entry : (Loc.t * vernac_control) option Gram.entry
+
+(** Handling of the proof mode entry *)
+val get_command_entry : unit -> vernac_expr Gram.entry
+val set_command_entry : vernac_expr Gram.entry -> unit
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index f001b572a..39c313ac7 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,10 +1,18 @@
+Vernacexpr
+Pvernac
+G_vernac
+G_proofs
 Vernacprop
-Proof_using
-Lemmas
 Himsg
 ExplainErr
-Class
 Locality
+Egramml
+Vernacinterp
+Ppvernac
+Proof_using
+Lemmas
+Class
+Egramcoq
 Metasyntax
 Auto_ind_decl
 Search
@@ -20,7 +28,6 @@ Classes
 Record
 Assumptions
 Vernacstate
-Vernacinterp
 Mltop
 Topfmt
 Vernacentries
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 65490bbbc..9a7f59085 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -977,7 +977,7 @@ let vernac_remove_hints ~atts dbs ids =
 
 let vernac_hints ~atts lb h =
   let local = enforce_module_locality atts.locality in
-  Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h)
+  Hints.add_hints ~local lb (Hints.interp_hints atts.polymorphic h)
 
 let vernac_syntactic_definition ~atts lid x y =
   Dumpglob.dump_definition lid false "syndef";
@@ -1971,7 +1971,7 @@ let vernac_load interp fname =
     interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
-    match Pcoq.Gram.entry_parse Pcoq.main_entry po with
+    match Pcoq.Gram.entry_parse Pvernac.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
diff --git a/parsing/vernacexpr.ml b/vernac/vernacexpr.ml
index 6ebf66349..cf0da4de2 100644
--- a/parsing/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -103,14 +103,16 @@ type comment =
   | CommentString of string
   | CommentInt of int
 
-type reference_or_constr =
+type reference_or_constr = Hints.reference_or_constr =
   | HintsReference of reference
   | HintsConstr of constr_expr
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
 
-type hint_mode =
+type hint_mode = Hints.hint_mode =
   | ModeInput (* No evars *)
   | ModeNoHeadEvar (* No evar at the head *)
   | ModeOutput (* Anything *)
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
 
 type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
     { hint_priority : int option;
@@ -120,14 +122,15 @@ type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
 type hint_info_expr = Typeclasses.hint_info_expr
 [@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"]
 
-type hints_expr =
-  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
-  | HintsImmediate of reference_or_constr list
+type hints_expr = Hints.hints_expr =
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * Hints.reference_or_constr) list
+  | HintsImmediate of Hints.reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
-  | HintsMode of reference * hint_mode list
+  | HintsMode of reference * Hints.hint_mode list
   | HintsConstructors of reference list
   | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
 
 type search_restriction =
   | SearchInside of reference list
@@ -401,7 +404,7 @@ type nonrec vernac_expr =
   (* Commands *)
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * reference list
-  | VernacHints of string list * hints_expr
+  | VernacHints of string list * Hints.hints_expr
   | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
       onlyparsing_flag
   | VernacArguments of reference or_by_notation *