[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, 10 insertions, 24 deletions

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