[api] Make `vernac/` self-contained.

We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.

IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.

The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.

This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.

1 files changed, 0 insertions, 41 deletions

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 *)