[api] Move `Vernacexpr` to parsing.

There were a few spurious dependencies on the `Vernac` AST in the
pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing,
where they do belong more.

3 files changed, 0 insertions, 666 deletions

diff --git a/pretyping/extend.ml b/pretyping/extend.ml
deleted file mode 100644
index 734b859f6..000000000
--- a/pretyping/extend.ml
+++ /dev/null
@@ -1,134 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-(** Entry keys for constr notations *)
-
-type 'a entry = 'a Grammar.GMake(CLexer).Entry.e
-
-type side = Left | Right
-
-type gram_assoc = NonA | RightA | LeftA
-
-type gram_position =
-  | First
-  | Last
-  | Before of string
-  | After of string
-  | Level of string
-
-type production_position =
-  | BorderProd of side * gram_assoc option
-  | InternalProd
-
-type production_level =
-  | NextLevel
-  | NumLevel of int
-
-type constr_as_binder_kind =
-  | AsIdent
-  | AsIdentOrPattern
-  | AsStrictPattern
-
-(** User-level types used to tell how to parse or interpret of the non-terminal *)
-
-type 'a constr_entry_key_gen =
-  | ETName
-  | ETReference
-  | ETBigint
-  | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
-  | ETConstr of 'a
-  | ETConstrAsBinder of constr_as_binder_kind * 'a
-  | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
-  | ETOther of string * string
-
-(** Entries level (left-hand side of grammar rules) *)
-
-type constr_entry_key =
-    (production_level * production_position) constr_entry_key_gen
-
-(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
-
-type simple_constr_prod_entry_key =
-    production_level option constr_entry_key_gen
-
-(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *)
-
-type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list
-
-type binder_target = ForBinder | ForTerm
-
-type constr_prod_entry_key =
-  | ETProdName            (* Parsed as a name (ident or _) *)
-  | ETProdReference       (* Parsed as a global reference *)
-  | ETProdBigint          (* Parsed as an (unbounded) integer *)
-  | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *)
-  | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
-  | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *)
-  | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *)
-  | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
-
-(** {5 AST for user-provided entries} *)
-
-type 'a user_symbol =
-| Ulist1 of 'a user_symbol
-| Ulist1sep of 'a user_symbol * string
-| Ulist0 of 'a user_symbol
-| Ulist0sep of 'a user_symbol * string
-| Uopt of 'a user_symbol
-| Uentry of 'a
-| Uentryl of 'a * int
-
-type ('a,'b,'c) ty_user_symbol =
-| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
-| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
-| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
-| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
-
-(** {5 Type-safe grammar extension} *)
-
-type ('self, 'a) symbol =
-| Atoken : Tok.t -> ('self, string) symbol
-| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol
-| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
-| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol
-| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
-| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
-| Aself : ('self, 'self) symbol
-| Anext : ('self, 'self) symbol
-| Aentry : 'a entry -> ('self, 'a) symbol
-| Aentryl : 'a entry * int -> ('self, 'a) symbol
-| Arules : 'a rules list -> ('self, 'a) symbol
-
-and ('self, _, 'r) rule =
-| Stop : ('self, 'r, 'r) rule
-| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule
-
-and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule }
-
-and 'a rules =
-| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
-
-type 'a production_rule =
-| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
-
-type 'a single_extend_statment =
-  string option *
-  (** Level *)
-  gram_assoc option *
-  (** Associativity *)
-  'a production_rule list
-  (** Symbol list with the interpretation function *)
-
-type 'a extend_statment =
-  gram_position option *
-  'a single_extend_statment list
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index d98026bc6..c48decdb0 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -27,8 +27,6 @@ Pattern
 Patternops
 Constr_matching
 Tacred
-Extend
-Vernacexpr
 Typeclasses_errors
 Typeclasses
 Classops
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
deleted file mode 100644
index 71a2e8cb8..000000000
--- a/pretyping/vernacexpr.ml
+++ /dev/null
@@ -1,530 +0,0 @@
-(************************************************************************)
-(*         *   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 Names
-open Misctypes
-open Constrexpr
-open Libnames
-
-(** Vernac expressions, produced by the parser *)
-type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
-
-type goal_selector = Goal_select.t =
-  | SelectAlreadyFocused
-  | SelectNth of int
-  | SelectList of (int * int) list
-  | SelectId of Id.t
-  | SelectAll
-[@@ocaml.deprecated "Use Goal_select.t"]
-
-type goal_identifier = string
-type scope_name = string
-
-type goal_reference =
-  | OpenSubgoals
-  | NthGoal of int
-  | GoalId of Id.t
-
-type univ_name_list = UnivNames.univ_name_list
-[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
-
-type printable =
-  | PrintTables
-  | PrintFullContext
-  | PrintSectionContext of reference
-  | PrintInspect of int
-  | PrintGrammar of string
-  | PrintLoadPath of DirPath.t option
-  | PrintModules
-  | PrintModule of reference
-  | PrintModuleType of reference
-  | PrintNamespace of DirPath.t
-  | PrintMLLoadPath
-  | PrintMLModules
-  | PrintDebugGC
-  | PrintName of reference or_by_notation * UnivNames.univ_name_list option
-  | PrintGraph
-  | PrintClasses
-  | PrintTypeClasses
-  | PrintInstances of reference or_by_notation
-  | PrintCoercions
-  | PrintCoercionPaths of class_rawexpr * class_rawexpr
-  | PrintCanonicalConversions
-  | PrintUniverses of bool * string option
-  | PrintHint of reference or_by_notation
-  | PrintHintGoal
-  | PrintHintDbName of string
-  | PrintHintDb
-  | PrintScopes
-  | PrintScope of string
-  | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
-  | PrintImplicit of reference or_by_notation
-  | PrintAssumptions of bool * bool * reference or_by_notation
-  | PrintStrategy of reference or_by_notation option
-
-type search_about_item =
-  | SearchSubPattern of constr_pattern_expr
-  | SearchString of string * scope_name option
-
-type searchable =
-  | SearchPattern of constr_pattern_expr
-  | SearchRewrite of constr_pattern_expr
-  | SearchHead of constr_pattern_expr
-  | SearchAbout of (bool * search_about_item) list
-
-type locatable =
-  | LocateAny of reference or_by_notation
-  | LocateTerm of reference or_by_notation
-  | LocateLibrary of reference
-  | LocateModule of reference
-  | LocateOther of string * reference
-  | LocateFile of string
-
-type showable =
-  | ShowGoal of goal_reference
-  | ShowProof
-  | ShowScript
-  | ShowExistentials
-  | ShowUniverses
-  | ShowProofNames
-  | ShowIntros of bool
-  | ShowMatch of reference
-
-type comment =
-  | CommentConstr of constr_expr
-  | CommentString of string
-  | CommentInt of int
-
-type reference_or_constr =
-  | HintsReference of reference
-  | HintsConstr of constr_expr
-
-type hint_mode =
-  | ModeInput (* No evars *)
-  | ModeNoHeadEvar (* No evar at the head *)
-  | ModeOutput (* Anything *)
-
-type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
-    { hint_priority : int option;
-      hint_pattern : 'a option }
-[@@ocaml.deprecated "Please use [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
-  | HintsUnfold of reference list
-  | HintsTransparency of reference list * bool
-  | HintsMode of reference * hint_mode list
-  | HintsConstructors of reference list
-  | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
-
-type search_restriction =
-  | SearchInside of reference list
-  | SearchOutside of reference list
-
-type rec_flag       = bool (* true = Rec;           false = NoRec          *)
-type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
-type opacity_flag   = Proof_global.opacity_flag = Opaque | Transparent
- [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"]
-type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
-type instance_flag  = bool option
-  (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
-type export_flag    = bool (* true = Export;        false = Import         *)
-type inductive_flag = Declarations.recursivity_kind
-type onlyparsing_flag = Flags.compat_version option
- (* Some v = Parse only;  None = Print also.
-    If v<>Current, it contains the name of the coq version
-    which this notation is trying to be compatible with *)
-type locality_flag  = bool (* true = Local *)
-
-type option_value = Goptions.option_value =
-  | BoolValue of bool
-  | IntValue of int option
-  | StringValue of string
-  | StringOptValue of string option
-
-type option_ref_value =
-  | StringRefValue of string
-  | QualidRefValue of reference
-
-(** Identifier and optional list of bound universes and constraints. *)
-
-type sort_expr = Sorts.family
-
-type definition_expr =
-  | ProveBody of local_binder_expr list * constr_expr
-  | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
-      * constr_expr option
-
-type fixpoint_expr =
-    ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
-
-type cofixpoint_expr =
-    ident_decl * local_binder_expr list * constr_expr * constr_expr option
-
-type local_decl_expr =
-  | AssumExpr of lname * constr_expr
-  | DefExpr of lname * constr_expr * constr_expr option
-
-type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *)
-type decl_notation = lstring * constr_expr * scope_name option
-type simple_binder = lident list  * constr_expr
-type class_binder = lident * constr_expr list
-type 'a with_coercion = coercion_flag * 'a
-type 'a with_instance = instance_flag * 'a
-type 'a with_notation = 'a * decl_notation list
-type 'a with_priority = 'a * int option
-type constructor_expr = (lident * constr_expr) with_coercion
-type constructor_list_or_record_decl_expr =
-  | Constructors of constructor_expr list
-  | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
-type inductive_expr =
-  ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
-    constructor_list_or_record_decl_expr
-
-type one_inductive_expr =
-  ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
-
-type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
-and typeclass_context = typeclass_constraint list
-
-type proof_expr =
-  ident_decl * (local_binder_expr list * constr_expr)
-
-type syntax_modifier =
-  | SetItemLevel of string list * Extend.production_level
-  | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option
-  | SetLevel of int
-  | SetAssoc of Extend.gram_assoc
-  | SetEntryType of string * Extend.simple_constr_prod_entry_key
-  | SetOnlyParsing
-  | SetOnlyPrinting
-  | SetCompatVersion of Flags.compat_version
-  | SetFormat of string * lstring
-
-type proof_end =
-  | Admitted
-  (*                         name in `Save ident` when closing goal *)
-  | Proved of opacity_flag * lident option
-
-type scheme =
-  | InductionScheme of bool * reference or_by_notation * sort_expr
-  | CaseScheme of bool * reference or_by_notation * sort_expr
-  | EqualityScheme of reference or_by_notation
-
-type section_subset_expr =
-  | SsEmpty
-  | SsType
-  | SsSingl of lident
-  | SsCompl of section_subset_expr
-  | SsUnion of section_subset_expr * section_subset_expr
-  | SsSubstr of section_subset_expr * section_subset_expr
-  | SsFwdClose of section_subset_expr
-
-(** Extension identifiers for the VERNAC EXTEND mechanism.
-
-    {b ("Extraction", 0} indicates {b Extraction {i qualid}} command.
-
-    {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command.
-
-    {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command.
-
-    {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command.
-
-    {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command.
-
-    {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command.
-
-    {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands.
-
-    {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command.
-
-    {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command.
-
-    {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command.
-
-    {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command.
-
-    {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command.
- *)
-type extend_name =
-  (** Name of the vernac entry where the tactic is defined, typically found
-      after the VERNAC EXTEND statement in the source. *)
-  string *
-  (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch
-      is given an offset, starting from zero. *)
-  int
-
-(* This type allows registering the inlining of constants in native compiler.
-   It will be extended with primitive inductive types and operators *)
-type register_kind =
-  | RegisterInline
-
-type bullet = Proof_bullet.t
-[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
-
-(** {6 Types concerning the module layer} *)
-
-(** Rigid / flexible module signature *)
-
-type 'a module_signature = 'a Declaremods.module_signature =
-  | Enforce of 'a (** ... : T *)
-  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
-[@@ocaml.deprecated "please use [Declaremods.module_signature]."]
-
-(** Which module inline annotations should we honor,
-    either None or the ones whose level is less or equal
-    to the given integer *)
-
-type inline = Declaremods.inline =
-  | NoInline
-  | DefaultInline
-  | InlineAt of int
-[@@ocaml.deprecated "please use [Declaremods.inline]."]
-
-type module_ast_inl = module_ast * Declaremods.inline
-type module_binder = bool option * lident list * module_ast_inl
-
-(** [Some b] if locally enabled/disabled according to [b], [None] if
-    we should use the global flag. *)
-type vernac_cumulative = VernacCumulative | VernacNonCumulative
-
-(** {6 The type of vernacular expressions} *)
-
-type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
-type vernac_argument_status = {
-  name : Name.t;
-  recarg_like : bool;
-  notation_scope : string CAst.t option;
-  implicit_status : vernac_implicit_status;
-}
-
-type nonrec vernac_expr =
-
-  | VernacLoad of verbose_flag * string
-  (* Syntax *)
-  | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
-  | VernacOpenCloseScope of bool * scope_name
-  | VernacDelimiters of scope_name * string option
-  | VernacBindScope of scope_name * class_rawexpr list
-  | VernacInfix of (lstring * syntax_modifier list) *
-      constr_expr * scope_name option
-  | VernacNotation of
-      constr_expr * (lstring * syntax_modifier list) *
-      scope_name option
-  | VernacNotationAddFormat of string * string * string
-
-  (* Gallina *)
-  | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
-  | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
-  | VernacEndProof of proof_end
-  | VernacExactProof of constr_expr
-  | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
-      Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
-  | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
-  | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
-  | VernacScheme of (lident option * scheme) list
-  | VernacCombinedScheme of lident * lident list
-  | VernacUniverse of lident list
-  | VernacConstraint of Glob_term.glob_constraint list
-
-  (* Gallina extensions *)
-  | VernacBeginSection of lident
-  | VernacEndSegment of lident
-  | VernacRequire of
-      reference option * export_flag option * reference list
-  | VernacImport of export_flag * reference list
-  | VernacCanonical of reference or_by_notation
-  | VernacCoercion of reference or_by_notation *
-      class_rawexpr * class_rawexpr
-  | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
-  | VernacNameSectionHypSet of lident * section_subset_expr 
-
-  (* Type classes *)
-  | VernacInstance of
-      bool * (* abstract instance *)
-      local_binder_expr list * (* super *)
-	typeclass_constraint * (* instance name, class name, params *)
-	(bool * constr_expr) option * (* props *)
-        Typeclasses.hint_info_expr
-
-  | VernacContext of local_binder_expr list
-
-  | VernacDeclareInstances of
-    (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *)
-
-  | VernacDeclareClass of reference (* inductive or definition name *)
-
-  (* Modules and Module Types *)
-  | VernacDeclareModule of bool option * lident *
-      module_binder list * module_ast_inl
-  | VernacDefineModule of bool option * lident * module_binder list *
-      module_ast_inl Declaremods.module_signature * module_ast_inl list
-  | VernacDeclareModuleType of lident *
-      module_binder list * module_ast_inl list * module_ast_inl list
-  | VernacInclude of module_ast_inl list
-
-  (* Solving *)
-
-  | VernacSolveExistential of int * constr_expr
-
-  (* Auxiliary file and library management *)
-  | VernacAddLoadPath of rec_flag * string * DirPath.t option
-  | VernacRemoveLoadPath of string
-  | VernacAddMLPath of rec_flag * string
-  | VernacDeclareMLModule of string list
-  | VernacChdir of string option
-
-  (* State management *)
-  | VernacWriteState of string
-  | VernacRestoreState of string
-
-  (* Resetting *)
-  | VernacResetName of lident
-  | VernacResetInitial
-  | VernacBack of int
-  | VernacBackTo of int
-
-  (* Commands *)
-  | VernacCreateHintDb of string * bool
-  | VernacRemoveHints of string list * reference list
-  | VernacHints of string list * hints_expr
-  | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
-      onlyparsing_flag
-  | VernacArguments of reference or_by_notation *
-      vernac_argument_status list (* Main arguments status list *) *
-        (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
-      int option (* Number of args to trigger reduction *) *
-        [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
-          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
-          `DefaultImplicits ] list
-  | VernacReserve of simple_binder list
-  | VernacGeneralizable of (lident list) option
-  | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
-  | VernacSetStrategy of
-      (Conv_oracle.level * reference or_by_notation list) list
-  | VernacUnsetOption of export_flag * Goptions.option_name
-  | VernacSetOption of export_flag * Goptions.option_name * option_value
-  | VernacAddOption of Goptions.option_name * option_ref_value list
-  | VernacRemoveOption of Goptions.option_name * option_ref_value list
-  | VernacMemOption of Goptions.option_name * option_ref_value list
-  | VernacPrintOption of Goptions.option_name
-  | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr
-  | VernacGlobalCheck of constr_expr
-  | VernacDeclareReduction of string * Genredexpr.raw_red_expr
-  | VernacPrint of printable
-  | VernacSearch of searchable * Goal_select.t option * search_restriction
-  | VernacLocate of locatable
-  | VernacRegister of lident * register_kind
-  | VernacComments of comment list
-
-  (* Proof management *)
-  | VernacAbort of lident option
-  | VernacAbortAll
-  | VernacRestart
-  | VernacUndo of int
-  | VernacUndoTo of int
-  | VernacFocus of int option
-  | VernacUnfocus
-  | VernacUnfocused
-  | VernacBullet of Proof_bullet.t
-  | VernacSubproof of Goal_select.t option
-  | VernacEndSubproof
-  | VernacShow of showable
-  | VernacCheckGuard
-  | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
-  | VernacProofMode of string
-
-  (* For extension *)
-  | VernacExtend of extend_name * Genarg.raw_generic_argument list
-
-type nonrec vernac_flag =
-  | VernacProgram
-  | VernacPolymorphic of bool
-  | VernacLocal of bool
-
-type vernac_control =
-  | VernacExpr of vernac_flag list * vernac_expr
-  (* boolean is true when the `-time` batch-mode command line flag was set.
-     the flag is used to print differently in `-time` vs `Time foo` *)
-  | VernacTime of bool * vernac_control CAst.t
-  | VernacRedirect of string * vernac_control CAst.t
-  | VernacTimeout of int * vernac_control
-  | VernacFail of vernac_control
-
-(* A vernac classifier provides information about the exectuion of a
-   command:
-
-   - vernac_when: encodes if the vernac may alter the parser [thus
-     forcing immediate execution], or if indeed it is pure and parsing
-     can continue without its execution.
-
-   - vernac_type: if it is starts, ends, continues a proof or
-     alters the global state or is a control command like BackTo or is
-     a query like Check.
-
-   The classification works on the assumption that we have 3 states:
-   parsing, execution (global enviroment, etc...), and proof
-   state. For example, commands that only alter the proof state are
-   considered safe to delegate to a worker.
-
-*)
-type vernac_type =
-  (* Start of a proof *)
-  | VtStartProof of vernac_start
-  (* Command altering the global state, bad for parallel
-     processing. *)
-  | VtSideff of vernac_sideff_type
-  (* End of a proof *)
-  | VtQed of vernac_qed_type
-  (* A proof step *)
-  | VtProofStep of proof_step
-  (* To be removed *)
-  | VtProofMode of string
-  (* Queries are commands assumed to be "pure", that is to say, they
-     don't modify the interpretation state. *)
-  | VtQuery
-  (* To be removed *)
-  | VtMeta
-  | VtUnknown
-and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
-and vernac_start = string * opacity_guarantee * Id.t list
-and vernac_sideff_type = Id.t list
-and opacity_guarantee =
-  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
-  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
-and proof_step = { (* TODO: inline with OCaml 4.03 *)
-  parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
-  proof_block_detection : proof_block_name option
-}
-and solving_tac = bool (* a terminator *)
-and anon_abstracting_tac = bool (* abstracting anonymously its result *)
-and proof_block_name = string (* open type of delimiters *)
-type vernac_when =
-  | VtNow
-  | VtLater
-type vernac_classification = vernac_type * vernac_when
-
-
-(** Deprecated stuff *)
-type universe_decl_expr = Constrexpr.universe_decl_expr
-[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"]
-
-type ident_decl = Constrexpr.ident_decl
-[@@ocaml.deprecated "alias of Constrexpr.ident_decl"]
-
-type name_decl = Constrexpr.name_decl
-[@@ocaml.deprecated "alias of Constrexpr.name_decl"]