[api] Relocate `intf` modules according to dependency-order.

In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.

We move all the files in `intf` to the lowest place their dependencies
can accommodate:

- `Misctypes`: is used by Declaremod, thus it has to go in `library`
  or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
  proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
  also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
  the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
  could be fixed, as this module should be declared in `interp` which
  is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
  as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.

Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...

8 files changed, 1146 insertions, 1 deletions

diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml
new file mode 100644
index 000000000..fda31756a
--- /dev/null
+++ b/pretyping/constrexpr.ml
@@ -0,0 +1,153 @@
+(************************************************************************)
+(*         *   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 Libnames
+open Misctypes
+open Decl_kinds
+
+(** {6 Concrete syntax for terms } *)
+
+(** [constr_expr] is the abstract syntax tree produced by the parser *)
+
+type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
+
+type ident_decl = lident * universe_decl_expr option
+type name_decl = lname * universe_decl_expr option
+
+type notation = string
+
+type explicitation =
+  | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
+  | ExplByName of Id.t
+
+type binder_kind =
+  | Default of binding_kind
+  | Generalized of binding_kind * binding_kind * bool
+      (** Inner binding, outer bindings, typeclass-specific flag
+	 for implicit generalization of superclasses *)
+
+type abstraction_kind = AbsLambda | AbsPi
+
+type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
+
+(** Representation of integer literals that appear in Coq scripts.
+    We now use raw strings of digits in base 10 (big-endian), and a separate
+    sign flag. Note that this representation is not unique, due to possible
+    multiple leading zeros, and -0 = +0 *)
+
+type sign = bool
+type raw_natural_number = string
+
+type prim_token =
+  | Numeral of raw_natural_number * sign
+  | String of string
+
+type instance_expr = Misctypes.glob_level list
+
+type cases_pattern_expr_r =
+  | CPatAlias of cases_pattern_expr * lname
+  | CPatCstr  of reference
+    * cases_pattern_expr list option * cases_pattern_expr list
+  (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
+  | CPatAtom of reference option
+  | CPatOr   of cases_pattern_expr list
+  | CPatNotation of notation * cases_pattern_notation_substitution
+    * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
+				  (notation n applied with substitution l1)
+				  applied to arguments l2 *)
+  | CPatPrim   of prim_token
+  | CPatRecord of (reference * cases_pattern_expr) list
+  | CPatDelimiters of string * cases_pattern_expr
+  | CPatCast   of cases_pattern_expr * constr_expr
+and cases_pattern_expr = cases_pattern_expr_r CAst.t
+
+and cases_pattern_notation_substitution =
+    cases_pattern_expr list *     (** for constr subterms *)
+    cases_pattern_expr list list  (** for recursive notations *)
+
+and constr_expr_r =
+  | CRef     of reference * instance_expr option
+  | CFix     of lident * fix_expr list
+  | CCoFix   of lident * cofix_expr list
+  | CProdN   of local_binder_expr list * constr_expr
+  | CLambdaN of local_binder_expr list * constr_expr
+  | CLetIn   of lname * constr_expr * constr_expr option * constr_expr
+  | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
+  | CApp     of (proj_flag * constr_expr) *
+                (constr_expr * explicitation CAst.t option) list
+  | CRecord  of (reference * constr_expr) list
+
+  (* representation of the "let" and "match" constructs *)
+  | CCases of Constr.case_style   (* determines whether this value represents "let" or "match" construct *)
+            * constr_expr option  (* return-clause *)
+            * case_expr list
+            * branch_expr list    (* branches *)
+
+  | CLetTuple of lname list * (lname option * constr_expr option) *
+                 constr_expr * constr_expr
+  | CIf of constr_expr * (lname option * constr_expr option)
+         * constr_expr * constr_expr
+  | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
+  | CPatVar of patvar
+  | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
+  | CSort   of glob_sort
+  | CCast   of constr_expr * constr_expr cast_type
+  | CNotation of notation * constr_notation_substitution
+  | CGeneralization of binding_kind * abstraction_kind option * constr_expr
+  | CPrim of prim_token
+  | CDelimiters of string * constr_expr
+  | CProj of reference * constr_expr
+and constr_expr = constr_expr_r CAst.t
+
+and case_expr = constr_expr                 (* expression that is being matched *)
+              * lname option                (* as-clause *)
+	      * cases_pattern_expr option   (* in-clause *)
+
+and branch_expr =
+  (cases_pattern_expr list list * constr_expr) CAst.t
+
+and fix_expr =
+    lident * (lident option * recursion_order_expr) *
+      local_binder_expr list * constr_expr * constr_expr
+
+and cofix_expr =
+    lident * local_binder_expr list * constr_expr * constr_expr
+
+and recursion_order_expr =
+  | CStructRec
+  | CWfRec of constr_expr
+  | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
+
+(* Anonymous defs allowed ?? *)
+and local_binder_expr =
+  | CLocalAssum   of lname list * binder_kind * constr_expr
+  | CLocalDef     of lname * constr_expr * constr_expr option
+  | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
+
+and constr_notation_substitution =
+    constr_expr list *      (** for constr subterms *)
+    constr_expr list list * (** for recursive notations *)
+    cases_pattern_expr list *   (** for binders *)
+    local_binder_expr list list (** for binder lists (recursive notations) *)
+
+type constr_pattern_expr = constr_expr
+
+(** Concrete syntax for modules and module types *)
+
+type with_declaration_ast =
+  | CWith_Module of Id.t list CAst.t * qualid CAst.t
+  | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
+
+type module_ast_r =
+  | CMident of qualid
+  | CMapply of module_ast * module_ast
+  | CMwith  of module_ast * with_declaration_ast
+and module_ast = module_ast_r CAst.t
diff --git a/pretyping/extend.ml b/pretyping/extend.ml
new file mode 100644
index 000000000..734b859f6
--- /dev/null
+++ b/pretyping/extend.ml
@@ -0,0 +1,134 @@
+(************************************************************************)
+(*         *   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/genredexpr.ml b/pretyping/genredexpr.ml
new file mode 100644
index 000000000..80697461a
--- /dev/null
+++ b/pretyping/genredexpr.ml
@@ -0,0 +1,66 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** Reduction expressions *)
+
+(** The parsing produces initially a list of [red_atom] *)
+
+type 'a red_atom =
+  | FBeta
+  | FMatch
+  | FFix
+  | FCofix
+  | FZeta
+  | FConst of 'a list
+  | FDeltaBut of 'a list
+
+(** This list of atoms is immediately converted to a [glob_red_flag] *)
+
+type 'a glob_red_flag = {
+  rBeta : bool;
+  rMatch : bool;
+  rFix : bool;
+  rCofix : bool;
+  rZeta : bool;
+  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
+  rConst : 'a list
+}
+
+(** Generic kinds of reductions *)
+
+type ('a,'b,'c) red_expr_gen =
+  | Red of bool
+  | Hnf
+  | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
+  | Cbv of 'b glob_red_flag
+  | Cbn of 'b glob_red_flag
+  | Lazy of 'b glob_red_flag
+  | Unfold of 'b Locus.with_occurrences list
+  | Fold of 'a list
+  | Pattern of 'a Locus.with_occurrences list
+  | ExtraRedExpr of string
+  | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
+  | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
+
+type ('a,'b,'c) may_eval =
+  | ConstrTerm of 'a
+  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
+  | ConstrContext of Misctypes.lident * 'a
+  | ConstrTypeOf of 'a
+
+open Libnames
+open Constrexpr
+open Misctypes
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = reference or_by_notation
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
new file mode 100644
index 000000000..84be15552
--- /dev/null
+++ b/pretyping/glob_term.ml
@@ -0,0 +1,113 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** Untyped intermediate terms *)
+
+(** [glob_constr] comes after [constr_expr] and before [constr].
+
+   Resolution of names, insertion of implicit arguments placeholder,
+   and notations are done, but coercions, inference of implicit
+   arguments and pattern-matching compilation are not. *)
+
+open Names
+open Globnames
+open Decl_kinds
+open Misctypes
+
+type existential_name = Id.t
+
+(**  The kind of patterns that occurs in "match ... with ... end"
+
+     locs here refers to the ident's location, not whole pat *)
+type 'a cases_pattern_r =
+  | PatVar  of Name.t
+  | PatCstr of constructor * 'a cases_pattern_g list * Name.t
+      (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
+and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
+
+type cases_pattern = [ `any ] cases_pattern_g
+
+(** Representation of an internalized (or in other words globalized) term. *)
+type 'a glob_constr_r =
+  | GRef of global_reference * glob_level list option
+      (** An identifier that represents a reference to an object defined
+          either in the (global) environment or in the (local) context. *)
+  | GVar of Id.t
+      (** An identifier that cannot be regarded as "GRef".
+          Bound variables are typically represented this way. *)
+  | GEvar   of existential_name * (Id.t * 'a glob_constr_g) list
+  | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
+  | GApp    of 'a glob_constr_g * 'a glob_constr_g list
+  | GLambda of Name.t * binding_kind *  'a glob_constr_g * 'a glob_constr_g
+  | GProd   of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g
+  | GLetIn  of Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g
+  | GCases  of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g
+      (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
+  | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
+  | GIf   of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
+  | GRec  of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
+             'a glob_constr_g array * 'a glob_constr_g array
+  | GSort of glob_sort
+  | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option
+  | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
+  | GProj of Projection.t * 'a glob_constr_g
+and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
+
+and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
+
+and 'a fix_recursion_order_g =
+  | GStructRec
+  | GWfRec of 'a glob_constr_g
+  | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option
+
+and 'a fix_kind_g =
+  | GFix of ((int option * 'a fix_recursion_order_g) array * int)
+  | GCoFix of int
+
+and 'a predicate_pattern_g =
+    Name.t * (inductive * Name.t list) CAst.t option
+      (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
+
+and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g)
+
+and 'a tomatch_tuples_g = 'a tomatch_tuple_g list
+
+and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.t
+(** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables
+    of [t] are members of [il]. *)
+and 'a cases_clauses_g = 'a cases_clause_g list
+
+type glob_constr = [ `any ] glob_constr_g
+type tomatch_tuple = [ `any ] tomatch_tuple_g
+type tomatch_tuples = [ `any ] tomatch_tuples_g
+type cases_clause = [ `any ] cases_clause_g
+type cases_clauses = [ `any ] cases_clauses_g
+type glob_decl = [ `any ] glob_decl_g
+type fix_kind = [ `any ] fix_kind_g
+type predicate_pattern = [ `any ] predicate_pattern_g
+type fix_recursion_order = [ `any ] fix_recursion_order_g
+
+type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
+
+type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) CAst.t
+type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list
+type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list
+
+type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g
+type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g
+type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g
+
+type 'a extended_glob_local_binder_r =
+  | GLocalAssum   of Name.t * binding_kind * 'a glob_constr_g
+  | GLocalDef     of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option
+  | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g
+and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t
+
+type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g
diff --git a/pretyping/locus.ml b/pretyping/locus.ml
new file mode 100644
index 000000000..95a2e495b
--- /dev/null
+++ b/pretyping/locus.ml
@@ -0,0 +1,96 @@
+(************************************************************************)
+(*         *   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
+
+(** Locus : positions in hypotheses and goals *)
+
+(** {6 Occurrences} *)
+
+type 'a occurrences_gen =
+  | AllOccurrences
+  | AllOccurrencesBut of 'a list (** non-empty *)
+  | NoOccurrences
+  | OnlyOccurrences of 'a list (** non-empty *)
+
+type occurrences_expr = (int or_var) occurrences_gen
+type 'a with_occurrences = occurrences_expr * 'a
+
+type occurrences = int occurrences_gen
+
+
+(** {6 Locations}
+
+  Selecting the occurrences in body (if any), in type, or in both *)
+
+type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly
+
+
+(** {6 Abstract clauses expressions}
+
+  A [clause_expr] (and its instance [clause]) denotes occurrences and
+  hypotheses in a goal in an abstract way; in particular, it can refer
+  to the set of all hypotheses independently of the effective contents
+  of the current goal
+
+  Concerning the field [onhyps]:
+   - [None] means *on every hypothesis*
+   - [Some l] means on hypothesis belonging to l *)
+
+type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
+
+type 'id clause_expr =
+  { onhyps : 'id hyp_location_expr list option;
+    concl_occs : occurrences_expr }
+
+type clause = Id.t clause_expr
+
+
+(** {6 Concrete view of occurrence clauses} *)
+
+(** [clause_atom] refers either to an hypothesis location (i.e. an
+   hypothesis with occurrences and a position, in body if any, in type
+   or in both) or to some occurrences of the conclusion *)
+
+type clause_atom =
+  | OnHyp of Id.t * occurrences_expr * hyp_location_flag
+  | OnConcl of occurrences_expr
+
+(** A [concrete_clause] is an effective collection of occurrences
+    in the hypotheses and the conclusion *)
+
+type concrete_clause = clause_atom list
+
+
+(** {6 A weaker form of clause with no mention of occurrences} *)
+
+(** A [hyp_location] is an hypothesis together with a location *)
+
+type hyp_location = Id.t * hyp_location_flag
+
+(** A [goal_location] is either an hypothesis (together with a location)
+    or the conclusion (represented by None) *)
+
+type goal_location = hyp_location option
+
+
+(** {6 Simple clauses, without occurrences nor location} *)
+
+(** A [simple_clause] is a set of hypotheses, possibly extended with
+   the conclusion (conclusion is represented by None) *)
+
+type simple_clause = Id.t option list
+
+(** {6 A notion of occurrences allowing to express "all occurrences
+       convertible to the first which matches"} *)
+
+type 'a or_like_first = AtOccs of 'a | LikeFirst
+
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
new file mode 100644
index 000000000..76367b612
--- /dev/null
+++ b/pretyping/pattern.ml
@@ -0,0 +1,43 @@
+(************************************************************************)
+(*         *   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 Globnames
+open Misctypes
+
+(** {5 Patterns} *)
+
+type case_info_pattern =
+    { cip_style : Constr.case_style;
+      cip_ind : inductive option;
+      cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *)
+      cip_extensible : bool (** does this match end with _ => _ ? *) }
+
+type constr_pattern =
+  | PRef of global_reference
+  | PVar of Id.t
+  | PEvar of existential_key * constr_pattern array
+  | PRel of int
+  | PApp of constr_pattern * constr_pattern array
+  | PSoApp of patvar * constr_pattern list
+  | PProj of Projection.t * constr_pattern
+  | PLambda of Name.t * constr_pattern * constr_pattern
+  | PProd of Name.t * constr_pattern * constr_pattern
+  | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
+  | PSort of glob_sort
+  | PMeta of patvar option
+  | PIf of constr_pattern * constr_pattern * constr_pattern
+  | PCase of case_info_pattern * constr_pattern * constr_pattern *
+      (int * bool list * constr_pattern) list (** index of constructor, nb of args *)
+  | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
+  | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
+
+(** Nota : in a [PCase], the array of branches might be shorter than
+    expected, denoting the use of a final "_ => _" branch *)
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index ae4ad0be7..d98026bc6 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,5 +1,5 @@
 Geninterp
-Ltac_pretype
+Locus
 Locusops
 Pretype_errors
 Reductionops
@@ -16,12 +16,19 @@ Evarsolve
 Recordops
 Evarconv
 Typing
+Constrexpr
+Genredexpr
 Miscops
+Glob_term
+Ltac_pretype
 Glob_ops
 Redops
+Pattern
 Patternops
 Constr_matching
 Tacred
+Extend
+Vernacexpr
 Typeclasses_errors
 Typeclasses
 Classops
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
new file mode 100644
index 000000000..4e1c986f1
--- /dev/null
+++ b/pretyping/vernacexpr.ml
@@ -0,0 +1,533 @@
+(************************************************************************)
+(*         *   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
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+   different type than [goal_reference] mostly because if it makes sense
+   to print a goal that is out of focus (or already solved) it doesn't
+   make sense to apply a tactic to it. Hence it the types may look very
+   similar, they do not seem to mean the same thing. *)
+type goal_selector =
+  | SelectNth of int
+  | SelectList of (int * int) list
+  | SelectId of Id.t
+  | SelectAll
+
+type goal_identifier = string
+type scope_name = string
+
+type goal_reference =
+  | OpenSubgoals
+  | NthGoal of int
+  | GoalId of Id.t
+
+type univ_name_list = Universes.univ_name_list
+[@@ocaml.deprecated "Use [Universes.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 * Universes.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 * Universes.univ_name_list option * goal_selector 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 =
+    { hint_priority : int option;
+      hint_pattern : 'a option }
+
+type hint_info_expr = constr_pattern_expr hint_info_gen
+
+type hints_expr =
+  | HintsResolve of (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   = Opaque | Transparent
+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 =
+    | Dash of int
+    | Star of int
+    | Plus of int
+
+(** {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_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 *)
+	hint_info_expr
+
+  | VernacContext of local_binder_expr list
+
+  | VernacDeclareInstances of
+    (reference * 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_selector option * constr_expr
+  | VernacGlobalCheck of constr_expr
+  | VernacDeclareReduction of string * Genredexpr.raw_red_expr
+  | VernacPrint of printable
+  | VernacSearch of searchable * goal_selector 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 bullet
+  | VernacSubproof of goal_selector 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"]