Imported Upstream version 8.5~beta1+dfsg

12 files changed, 1693 insertions, 0 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
new file mode 100644
index 00000000..79f4e99e
--- /dev/null
+++ b/intf/constrexpr.mli
@@ -0,0 +1,139 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+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 notation = string
+
+type explicitation =
+  | ExplByPos of int * Id.t option
+  | 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 *)
+
+type prim_token = Numeral of Bigint.bigint | String of string
+
+type raw_cases_pattern_expr =
+  | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
+  | RCPatCstr of Loc.t * Globnames.global_reference
+    * raw_cases_pattern_expr list * raw_cases_pattern_expr list
+  (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
+  | RCPatAtom of Loc.t * Id.t option
+  | RCPatOr of Loc.t * raw_cases_pattern_expr list
+
+type cases_pattern_expr =
+  | CPatAlias of Loc.t * cases_pattern_expr * Id.t
+  | CPatCstr of Loc.t * reference
+    * cases_pattern_expr list * cases_pattern_expr list
+  (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
+  | CPatAtom of Loc.t * reference option
+  | CPatOr of Loc.t * cases_pattern_expr list
+  | CPatNotation of Loc.t * 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 Loc.t * prim_token
+  | CPatRecord of Loc.t * (reference * cases_pattern_expr) list
+  | CPatDelimiters of Loc.t * string * cases_pattern_expr
+
+and cases_pattern_notation_substitution =
+    cases_pattern_expr list *     (** for constr subterms *)
+    cases_pattern_expr list list  (** for recursive notations *)
+
+type instance_expr = Misctypes.glob_level list
+
+type constr_expr =
+  | CRef of reference * instance_expr option
+  | CFix of Loc.t * Id.t located * fix_expr list
+  | CCoFix of Loc.t * Id.t located * cofix_expr list
+  | CProdN of Loc.t * binder_expr list * constr_expr
+  | CLambdaN of Loc.t * binder_expr list * constr_expr
+  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr
+  | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list
+  | CApp of Loc.t * (proj_flag * constr_expr) *
+      (constr_expr * explicitation located option) list
+  | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list
+  | CCases of Loc.t * case_style * constr_expr option *
+      case_expr list * branch_expr list
+  | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) *
+      constr_expr * constr_expr
+  | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option)
+      * constr_expr * constr_expr
+  | CHole of Loc.t * Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
+  | CPatVar of Loc.t * patvar
+  | CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list
+  | CSort of Loc.t * glob_sort
+  | CCast of Loc.t * constr_expr * constr_expr cast_type
+  | CNotation of Loc.t * notation * constr_notation_substitution
+  | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr
+  | CPrim of Loc.t * prim_token
+  | CDelimiters of Loc.t * string * constr_expr
+
+and case_expr =
+  constr_expr * (Name.t located option * cases_pattern_expr option)
+
+and branch_expr =
+  Loc.t * cases_pattern_expr list located list * constr_expr
+
+and binder_expr =
+  Name.t located list * binder_kind * constr_expr
+
+and fix_expr =
+    Id.t located * (Id.t located option * recursion_order_expr) *
+      local_binder list * constr_expr * constr_expr
+
+and cofix_expr =
+    Id.t located * local_binder 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 =
+  | LocalRawDef of Name.t located * constr_expr
+  | LocalRawAssum of Name.t located list * binder_kind * constr_expr
+
+and constr_notation_substitution =
+    constr_expr list *      (** for constr subterms *)
+    constr_expr list list * (** for recursive notations *)
+    local_binder list list (** for binders subexpressions *)
+
+type typeclass_constraint = Name.t located * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
+
+type constr_pattern_expr = constr_expr
+
+(** Concrete syntax for modules and module types *)
+
+type with_declaration_ast =
+  | CWith_Module of Id.t list located * qualid located
+  | CWith_Definition of Id.t list located * constr_expr
+
+type module_ast =
+  | CMident of qualid located
+  | CMapply of Loc.t * module_ast * module_ast
+  | CMwith of Loc.t * module_ast * with_declaration_ast
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
new file mode 100644
index 00000000..6886083c
--- /dev/null
+++ b/intf/decl_kinds.mli
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Informal mathematical status of declarations *)
+
+type locality = Discharge | Local | Global
+
+type binding_kind = Explicit | Implicit
+
+type polymorphic = bool
+
+type private_flag = bool 
+
+type theorem_kind =
+  | Theorem
+  | Lemma
+  | Fact
+  | Remark
+  | Property
+  | Proposition
+  | Corollary
+
+type definition_object_kind =
+  | Definition
+  | Coercion
+  | SubClass
+  | CanonicalStructure
+  | Example
+  | Fixpoint
+  | CoFixpoint
+  | Scheme
+  | StructureComponent
+  | IdentityCoercion
+  | Instance
+  | Method
+
+type assumption_object_kind = Definitional | Logical | Conjectural
+
+(** [assumption_kind]
+
+                |  Local      | Global
+   ------------------------------------
+   Definitional |  Variable   | Parameter
+   Logical      |  Hypothesis | Axiom
+
+*)
+type assumption_kind = locality * polymorphic * assumption_object_kind
+
+type definition_kind = locality * polymorphic * definition_object_kind
+
+(** Kinds used in proofs *)
+
+type goal_object_kind =
+  | DefinitionBody of definition_object_kind
+  | Proof of theorem_kind
+
+type goal_kind = locality * polymorphic * goal_object_kind
+
+(** Kinds used in library *)
+
+type logical_kind =
+  | IsAssumption of assumption_object_kind
+  | IsDefinition of definition_object_kind
+  | IsProof of theorem_kind
+
+(** Recursive power of type declarations *)
+
+type recursivity_kind =
+  | Finite (** = inductive *)
+  | CoFinite (** = coinductive *)
+  | BiFinite (** = non-recursive, like in "Record" definitions *)
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
new file mode 100644
index 00000000..38a3e81f
--- /dev/null
+++ b/intf/evar_kinds.mli
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Globnames
+
+(** The kinds of existential variable *)
+
+(** Should the obligation be defined (opaque or transparent (default)) or
+    defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
+type t =
+  | ImplicitArg of global_reference * (int * Id.t option)
+     * bool (** Force inference *)
+  | BinderType of Name.t
+  | QuestionMark of obligation_definition_status
+  | CasesType of bool (* true = a subterm of the type *)
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+  | GoalEvar
+  | ImpossibleCase
+  | MatchingVar of bool * Id.t
+  | VarInstance of Id.t
+  | SubEvar of Constr.existential_key
diff --git a/intf/extend.mli b/intf/extend.mli
new file mode 100644
index 00000000..ad9706f3
--- /dev/null
+++ b/intf/extend.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Entry keys for constr notations *)
+
+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 ('lev,'pos) constr_entry_key_gen =
+  | ETName | ETReference | ETBigint
+  | ETBinder of bool
+  | ETConstr of ('lev * 'pos)
+  | ETPattern
+  | ETOther of string * string
+  | ETConstrList of ('lev * 'pos) * Tok.t list
+  | ETBinderList of bool * Tok.t list
+
+(** Entries level (left-hand-side of grammar rules) *)
+
+type constr_entry_key =
+    (int,unit) constr_entry_key_gen
+
+(** Entries used in productions (in right-hand-side of grammar rules) *)
+
+type constr_prod_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,unit) constr_entry_key_gen
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
new file mode 100644
index 00000000..61340914
--- /dev/null
+++ b/intf/genredexpr.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Reduction expressions *)
+
+(** The parsing produces initially a list of [red_atom] *)
+
+type 'a red_atom =
+  | FBeta
+  | FIota
+  | 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;
+  rIota : 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 (Loc.t * Names.Id.t) * 'a
+  | ConstrTypeOf of 'a
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
new file mode 100644
index 00000000..32cf9eaf
--- /dev/null
+++ b/intf/glob_term.mli
@@ -0,0 +1,86 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** 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 cases_pattern =
+  | PatVar of Loc.t * Name.t
+  | PatCstr of Loc.t * constructor * cases_pattern list * Name.t
+      (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
+
+type glob_constr =
+  | GRef of (Loc.t * global_reference * glob_level list option)
+  | GVar of (Loc.t * Id.t)
+  | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list
+  | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
+  | GApp of Loc.t * glob_constr * glob_constr list
+  | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
+  | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
+  | GLetIn of Loc.t * Name.t * glob_constr * glob_constr
+  | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
+      (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in
+	  [MatchStyle]) *)
+  | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) *
+      glob_constr * glob_constr
+  | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr
+  | GRec of Loc.t * fix_kind * Id.t array * glob_decl list array *
+      glob_constr array * glob_constr array
+  | GSort of Loc.t * glob_sort
+  | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option)
+  | GCast of Loc.t * glob_constr * glob_constr cast_type
+
+and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr
+
+and fix_recursion_order =
+  | GStructRec
+  | GWfRec of glob_constr
+  | GMeasureRec of glob_constr * glob_constr option
+
+and fix_kind =
+  | GFix of ((int option * fix_recursion_order) array * int)
+  | GCoFix of int
+
+and predicate_pattern =
+    Name.t * (Loc.t * inductive * Name.t list) option
+      (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
+
+and tomatch_tuple = (glob_constr * predicate_pattern)
+
+and tomatch_tuples = tomatch_tuple list
+
+and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr)
+(** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables
+    of [t] are members of [il]. *)
+and cases_clauses = cases_clause list
+
+(** A globalised term together with a closure representing the value
+    of its free variables. Intended for use when these variables are taken
+    from the Ltac environment. *)
+type closure = {
+  idents:Id.t Id.Map.t;
+  typed: Pattern.constr_under_binders Id.Map.t ;
+  untyped:closed_glob_constr Id.Map.t }
+and closed_glob_constr = {
+  closure: closure;
+  term: glob_constr }
diff --git a/intf/locus.mli b/intf/locus.mli
new file mode 100644
index 00000000..80857794
--- /dev/null
+++ b/intf/locus.mli
@@ -0,0 +1,94 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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/intf/misctypes.mli b/intf/misctypes.mli
new file mode 100644
index 00000000..74e13690
--- /dev/null
+++ b/intf/misctypes.mli
@@ -0,0 +1,106 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+
+(** Basic types used both in [constr_expr] and in [glob_constr] *)
+
+(** Cases pattern variables *)
+
+type patvar = Id.t
+
+(** Introduction patterns *)
+
+type 'constr intro_pattern_expr =
+  | IntroForthcoming of bool
+  | IntroNaming of intro_pattern_naming_expr
+  | IntroAction of 'constr intro_pattern_action_expr
+and intro_pattern_naming_expr =
+  | IntroIdentifier of Id.t
+  | IntroFresh of Id.t
+  | IntroAnonymous
+and 'constr intro_pattern_action_expr =
+  | IntroWildcard
+  | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
+  | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list
+  | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr)
+  | IntroRewrite of bool
+and 'constr or_and_intro_pattern_expr =
+  (Loc.t * 'constr intro_pattern_expr) list list
+
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+(** Sorts *)
+
+type 'a glob_sort_gen = GProp | GSet | GType of 'a
+type sort_info = string list
+type level_info = string option
+
+type glob_sort = sort_info glob_sort_gen
+type glob_level = level_info glob_sort_gen
+
+(** A synonym of [Evar.t], also defined in Term *)
+
+type existential_key = Evar.t
+
+(** Case style, shared with Term *)
+
+type case_style = Term.case_style =
+  | LetStyle
+  | IfStyle
+  | LetPatternStyle
+  | MatchStyle
+  | RegularStyle (** infer printing form from number of constructor *)
+
+(** Casts *)
+
+type 'a cast_type =
+  | CastConv of 'a
+  | CastVM of 'a
+  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
+  | CastNative of 'a
+
+(** Bindings *)
+
+type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
+
+type 'a explicit_bindings = (Loc.t * quantified_hypothesis * 'a) list
+
+type 'a bindings =
+  | ImplicitBindings of 'a list
+  | ExplicitBindings of 'a explicit_bindings
+  | NoBindings
+
+type 'a with_bindings = 'a * 'a bindings
+
+
+(** Some utility types for parsing *)
+
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of Names.Id.t Loc.located
+
+type 'a and_short_name = 'a * Id.t Loc.located option
+
+type 'a or_by_notation =
+  | AN of 'a
+  | ByNotation of (Loc.t * string * string option)
+
+(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
+   but this formulation avoids a useless dependency. *)
+
+
+(** Kinds of modules *)
+
+type module_kind = Module | ModType | ModAny
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
new file mode 100644
index 00000000..5a563bf9
--- /dev/null
+++ b/intf/notation_term.mli
@@ -0,0 +1,81 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Globnames
+open Misctypes
+open Glob_term
+
+(** [notation_constr] *)
+
+(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic
+    extensions (i.e. notations).
+    No location since intended to be substituted at any place of a text.
+    Complex expressions such as fixpoints and cofixpoints are excluded,
+    as well as non global expressions such as existential variables. *)
+
+type notation_constr =
+  (** Part common to [glob_constr] and [cases_pattern] *)
+  | NRef of global_reference
+  | NVar of Id.t
+  | NApp of notation_constr * notation_constr list
+  | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
+  | NList of Id.t * Id.t * notation_constr * notation_constr * bool
+  (** Part only in [glob_constr] *)
+  | NLambda of Name.t * notation_constr * notation_constr
+  | NProd of Name.t * notation_constr * notation_constr
+  | NBinderList of Id.t * Id.t * notation_constr * notation_constr
+  | NLetIn of Name.t * notation_constr * notation_constr
+  | NCases of case_style * notation_constr option *
+      (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
+      (cases_pattern list * notation_constr) list
+  | NLetTuple of Name.t list * (Name.t * notation_constr option) *
+      notation_constr * notation_constr
+  | NIf of notation_constr * (Name.t * notation_constr option) *
+      notation_constr * notation_constr
+  | NRec of fix_kind * Id.t array *
+      (Name.t * notation_constr option * notation_constr) list array *
+      notation_constr array * notation_constr array
+  | NSort of glob_sort
+  | NPatVar of patvar
+  | NCast of notation_constr * notation_constr cast_type
+
+(** Note concerning NList: first constr is iterator, second is terminator;
+    first id is where each argument of the list has to be substituted
+    in iterator and snd id is alternative name just for printing;
+    boolean is associativity *)
+
+(** Types concerning notations *)
+
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
+    x carries the sequence of objects bound to the list x..y  *)
+type notation_var_instance_type =
+  | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
+
+(** Type of variables when interpreting a constr_expr as an notation_constr:
+    in a recursive pattern x..y, both x and y carry the individual type
+    of each element of the list x..y *)
+type notation_var_internalization_type =
+  | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
+
+(** This characterizes to what a notation is interpreted to *)
+type interpretation =
+    (Id.t * (subscopes * notation_var_instance_type)) list *
+    notation_constr
+
+type notation_interp_env = {
+  ninterp_var_type : notation_var_internalization_type Id.Map.t;
+  ninterp_rec_vars : Id.t Id.Map.t;
+  mutable ninterp_only_parse : bool;
+}
diff --git a/intf/pattern.mli b/intf/pattern.mli
new file mode 100644
index 00000000..18cd2df0
--- /dev/null
+++ b/intf/pattern.mli
@@ -0,0 +1,81 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Globnames
+open Term
+open Misctypes
+
+(** {5 Maps of pattern variables} *)
+
+(** Type [constr_under_binders] is for representing the term resulting
+    of a matching. Matching can return terms defined in a some context
+    of named binders; in the context, variable names are ordered by
+    (<) and referred to by index in the term Thanks to the canonical
+    ordering, a matching problem like
+
+    [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
+
+    will be accepted. Thanks to the reference by index, a matching
+    problem like
+
+    [match ... with [(fun x => ?p)] => [forall x => p]]
+
+    will work even if [x] is also the name of an existing goal
+    variable.
+
+    Note: we do not keep types in the signature. Besides simplicity,
+    the main reason is that it would force to close the signature over
+    binders that occur only in the types of effective binders but not
+    in the term itself (e.g. for a term [f x] with [f:A -> True] and
+    [x:A]).
+
+    On the opposite side, by not keeping the types, we loose
+    opportunity to propagate type informations which otherwise would
+    not be inferable, as e.g. when matching [forall x, x = 0] with
+    pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
+    expression [forall x, h = x] where nothing tells how the type of x
+    could be inferred. We also loose the ability of typing ltac
+    variables before calling the right-hand-side of ltac matching clauses. *)
+
+type constr_under_binders = Id.t list * constr
+
+(** Types of substitutions with or w/o bound variables *)
+
+type patvar_map = constr Id.Map.t
+type extended_patvar_map = constr_under_binders Id.Map.t
+
+(** {5 Patterns} *)
+
+type case_info_pattern =
+    { cip_style : 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 * 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
+  | 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 fixpoint
+  | PCoFix of cofixpoint
+
+(** Nota : in a [PCase], the array of branches might be shorter than
+    expected, denoting the use of a final "_ => _" branch *)
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
new file mode 100644
index 00000000..7b9ad313
--- /dev/null
+++ b/intf/tacexpr.mli
@@ -0,0 +1,415 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+open Names
+open Constrexpr
+open Libnames
+open Globnames
+open Nametab
+open Genredexpr
+open Genarg
+open Pattern
+open Decl_kinds
+open Misctypes
+open Locus
+
+type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
+type lazy_flag =
+  | General (* returns all possible successes *)
+  | Select  (* returns all successes of the first matching branch *)
+  | Once    (* returns the first success in a maching branch
+               (not necessarily the first) *)
+type global_flag = (* [gfail] or [fail] *)
+  | TacGlobal
+  | TacLocal
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+type rec_flag = bool       (* true = recursive        false = not recursive *)
+type advanced_flag = bool  (* true = advanced         false = basic *)
+type letin_flag = bool     (* true = use local def    false = use Leibniz *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
+type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
+
+type 'a core_induction_arg =
+  | ElimOnConstr of 'a
+  | ElimOnIdent of Id.t located
+  | ElimOnAnonHyp of int
+
+type 'a induction_arg =
+  clear_flag * 'a core_induction_arg
+
+type inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear
+
+type ('c,'d,'id) inversion_strength =
+  | NonDepInversion of
+      inversion_kind * 'id list * 'd or_and_intro_pattern_expr located or_var option
+  | DepInversion of
+      inversion_kind * 'c option * 'd or_and_intro_pattern_expr located or_var option
+  | InversionUsing of 'c * 'id list
+
+type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
+
+type 'id message_token =
+  | MsgString of string
+  | MsgInt of int
+  | MsgIdent of 'id
+
+type ('dconstr,'id) induction_clause =
+    'dconstr with_bindings induction_arg *
+    (intro_pattern_naming_expr located option (* eqn:... *)
+    * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *)
+    * 'id clause_expr option (* in ... *)
+
+type ('constr,'dconstr,'id) induction_clause_list =
+    ('dconstr,'id) induction_clause list
+    * 'constr with_bindings option (* using ... *)
+
+type 'a with_bindings_arg = clear_flag * 'a with_bindings
+
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
+(* Type of patterns *)
+type 'a match_pattern =
+  | Term of 'a
+  | Subterm of bool * Id.t option * 'a
+
+(* Type of hypotheses for a Match Context rule *)
+type 'a match_context_hyps =
+  | Hyp of Name.t located * 'a match_pattern
+  | Def of Name.t located * 'a match_pattern * 'a match_pattern
+
+(* Type of a Match rule for Match Context and Match *)
+type ('a,'t) match_rule =
+  | Pat of 'a match_context_hyps list * 'a match_pattern * 't
+  | All of 't
+
+type ml_tactic_name = {
+  mltac_plugin : string;
+  mltac_tactic : string;
+}
+
+(** Composite types *)
+
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+   in the environment by the effective calls to Intro, Inversion, etc 
+   The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
+
+type open_constr_expr = unit * constr_expr
+type open_glob_constr = unit * glob_constr_and_expr
+
+type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
+
+type delayed_open_constr_with_bindings =
+    Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings
+
+type delayed_open_constr =
+    Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr
+
+type intro_pattern = delayed_open_constr intro_pattern_expr located
+type intro_patterns = delayed_open_constr intro_pattern_expr located list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
+type intro_pattern_naming = intro_pattern_naming_expr located
+
+(** Generic expressions for atomic tactics *)
+
+type 'a gen_atomic_tactic_expr =
+  (* Basic tactics *)
+  | TacIntroPattern of 'dtrm intro_pattern_expr located list
+  | TacIntroMove of Id.t option * 'nam move_location
+  | TacExact of 'trm
+  | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
+      (clear_flag * 'nam * 'dtrm intro_pattern_expr located option) option
+  | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
+  | TacCase of evars_flag * 'trm with_bindings_arg
+  | TacFix of Id.t option * int
+  | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
+  | TacCofix of Id.t option
+  | TacMutualCofix of Id.t * (Id.t * 'trm) list
+  | TacAssert of
+      bool * 'tacexpr option *
+      'dtrm intro_pattern_expr located option * 'trm
+  | TacGeneralize of ('trm with_occurrences * Name.t) list
+  | TacGeneralizeDep of 'trm
+  | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
+      intro_pattern_naming_expr located option
+
+  (* Derived basic tactics *)
+  | TacInductionDestruct of
+      rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
+  | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
+
+  (* Automation tactics *)
+  | TacTrivial of debug * 'trm list * string list option
+  | TacAuto of debug * int or_var option * 'trm list * string list option
+
+  (* Context management *)
+  | TacClear of bool * 'nam list
+  | TacClearBody of 'nam list
+  | TacMove of 'nam * 'nam move_location
+  | TacRename of ('nam *'nam) list
+
+  (* Trmuctors *)
+  | TacSplit of evars_flag * 'trm bindings list
+
+  (* Conversion *)
+  | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
+  | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+
+  (* Equivalence relations *)
+  | TacSymmetry of 'nam clause_expr
+
+  (* Equality and inversion *)
+  | TacRewrite of evars_flag *
+      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (* spiwack: using ['dtrm] here is a small hack, may not be
+         stable by a change in the representation of delayed
+         terms. Because, in fact, it is the whole "with_bindings"
+         which is delayed. But because the "t" level for ['dtrm] is
+         uninterpreted, it works fine here too, and avoid more
+         disruption of this file. *)
+      'tacexpr option
+  | TacInversion of ('trm,'dtrm,'nam) inversion_strength * quantified_hypothesis
+
+constraint 'a = <
+    term:'trm;
+    utrm: 'utrm;
+    dterm: 'dtrm;
+    pattern:'pat;
+    constant:'cst;
+    reference:'ref;
+    name:'nam;
+    tacexpr:'tacexpr;
+    level:'lev
+>
+
+(** Possible arguments of a tactic definition *)
+
+and 'a gen_tactic_arg =
+  | TacDynamic     of Loc.t * Dyn.t
+  | TacGeneric     of 'lev generic_argument
+  | MetaIdArg      of Loc.t * bool * string
+  | ConstrMayEval  of ('trm,'cst,'pat) may_eval
+  | UConstr        of 'utrm
+  | Reference      of 'ref
+  | TacCall of Loc.t * 'ref *
+      'a gen_tactic_arg list
+  | TacFreshId of string or_var list
+  | Tacexp of 'tacexpr
+  | TacPretype of 'trm
+  | TacNumgoals
+
+constraint 'a = <
+    term:'trm;
+    utrm: 'utrm;
+    dterm: 'dtrm;
+    pattern:'pat;
+    constant:'cst;
+    reference:'ref;
+    name:'nam;
+    tacexpr:'tacexpr;
+    level:'lev
+>
+
+(** Generic ltac expressions.
+    't : terms, 'p : patterns, 'c : constants, 'i : inductive,
+    'r : ltac refs, 'n : idents, 'l : levels *)
+
+and 'a gen_tactic_expr =
+  | TacAtom of Loc.t * 'a gen_atomic_tactic_expr
+  | TacThen of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacDispatch of
+      'a gen_tactic_expr list
+  | TacExtendTac of
+      'a gen_tactic_expr array *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array
+  | TacThens of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr list
+  | TacThens3parts of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array
+  | TacFirst of 'a gen_tactic_expr list
+  | TacComplete of 'a gen_tactic_expr
+  | TacSolve of 'a gen_tactic_expr list
+  | TacTry of 'a gen_tactic_expr
+  | TacOr of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacOnce of
+      'a gen_tactic_expr
+  | TacExactlyOnce of
+      'a gen_tactic_expr
+  | TacIfThenCatch of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacOrelse of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacDo of int or_var * 'a gen_tactic_expr
+  | TacTimeout of int or_var * 'a gen_tactic_expr
+  | TacTime of string option * 'a gen_tactic_expr
+  | TacRepeat of 'a gen_tactic_expr
+  | TacProgress of 'a gen_tactic_expr
+  | TacShowHyps of 'a gen_tactic_expr
+  | TacAbstract of
+      'a gen_tactic_expr * Id.t option
+  | TacId of 'n message_token list
+  | TacFail of global_flag * int or_var * 'n message_token list
+  | TacInfo of 'a gen_tactic_expr
+  | TacLetIn of rec_flag *
+      (Id.t located * 'a gen_tactic_arg) list *
+      'a gen_tactic_expr
+  | TacMatch of lazy_flag *
+      'a gen_tactic_expr *
+      ('p,'a gen_tactic_expr) match_rule list
+  | TacMatchGoal of lazy_flag * direction_flag *
+      ('p,'a gen_tactic_expr) match_rule list
+  | TacFun of 'a gen_tactic_fun_ast
+  | TacArg of 'a gen_tactic_arg located
+  (* For ML extensions *)
+  | TacML of Loc.t * ml_tactic_name * 'l generic_argument list
+  (* For syntax extensions *)
+  | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list
+
+constraint 'a = <
+    term:'t;
+    utrm: 'utrm;
+    dterm: 'dtrm;
+    pattern:'p;
+    constant:'c;
+    reference:'r;
+    name:'n;
+    tacexpr:'tacexpr;
+    level:'l
+>
+
+and 'a gen_tactic_fun_ast =
+    Id.t option list * 'a gen_tactic_expr
+
+constraint 'a = <
+    term:'t;
+    utrm: 'utrm;
+    dterm: 'dtrm;
+    pattern:'p;
+    constant:'c;
+    reference:'r;
+    name:'n;
+    tacexpr:'te;
+    level:'l
+>
+
+(** Globalized tactics *)
+
+type g_trm = glob_constr_and_expr
+type g_utrm = g_trm
+type g_pat = glob_constr_and_expr * constr_pattern
+type g_cst = evaluable_global_reference and_short_name or_var
+type g_ref = ltac_constant located or_var
+type g_nam  = Id.t located
+
+type g_dispatch =  <
+    term:g_trm;
+    utrm:g_utrm;
+    dterm:g_trm;
+    pattern:g_pat;
+    constant:g_cst;
+    reference:g_ref;
+    name:g_nam;
+    tacexpr:glob_tactic_expr;
+    level:glevel
+>
+
+and glob_tactic_expr =
+    g_dispatch gen_tactic_expr
+
+type glob_atomic_tactic_expr =
+    g_dispatch gen_atomic_tactic_expr
+
+type glob_tactic_arg =
+    g_dispatch gen_tactic_arg
+
+(** Raw tactics *)
+
+type r_trm = constr_expr
+type r_utrm = r_trm
+type r_pat = constr_pattern_expr
+type r_cst = reference or_by_notation
+type r_ref = reference
+type r_nam  = Id.t located
+type r_lev = rlevel
+
+type r_dispatch =  <
+    term:r_trm;
+    utrm:r_utrm;
+    dterm:r_trm;
+    pattern:r_pat;
+    constant:r_cst;
+    reference:r_ref;
+    name:r_nam;
+    tacexpr:raw_tactic_expr;
+    level:rlevel
+>
+
+and raw_tactic_expr =
+    r_dispatch gen_tactic_expr
+
+type raw_atomic_tactic_expr =
+    r_dispatch gen_atomic_tactic_expr
+
+type raw_tactic_arg =
+    r_dispatch gen_tactic_arg
+
+(** Interpreted tactics *)
+
+type t_trm = Term.constr
+type t_utrm = Glob_term.closed_glob_constr
+type t_pat = glob_constr_and_expr * constr_pattern
+type t_cst = evaluable_global_reference and_short_name
+type t_ref = ltac_constant located
+type t_nam  = Id.t
+
+type t_dispatch =  <
+    term:t_trm;
+    utrm:t_utrm;
+    dterm:g_trm;
+    pattern:t_pat;
+    constant:t_cst;
+    reference:t_ref;
+    name:t_nam;
+    tacexpr:glob_tactic_expr;
+    level:tlevel
+>
+
+type tactic_expr =
+    t_dispatch gen_tactic_expr
+
+type atomic_tactic_expr =
+    t_dispatch gen_atomic_tactic_expr
+
+type tactic_arg =
+    t_dispatch gen_tactic_arg
+
+(** Misc *)
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
+type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
new file mode 100644
index 00000000..3f2d002c
--- /dev/null
+++ b/intf/vernacexpr.mli
@@ -0,0 +1,482 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+open Names
+open Tacexpr
+open Misctypes
+open Constrexpr
+open Decl_kinds
+open Libnames
+
+(** Vernac expressions, produced by the parser *)
+
+type lident = Id.t located
+type lname = Name.t located
+type lstring = string located
+type lreference = reference
+
+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
+  | SelectId of Id.t
+  | SelectAll
+  | SelectAllParallel
+
+type goal_identifier = string
+type scope_name = string
+
+type goal_reference =
+  | OpenSubgoals
+  | NthGoal of int
+  | GoalId of goal_identifier
+
+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
+  | PrintGraph
+  | PrintClasses
+  | PrintTypeClasses
+  | PrintInstances of reference or_by_notation
+  | PrintLtac of reference
+  | PrintCoercions
+  | PrintCoercionPaths of class_rawexpr * class_rawexpr
+  | PrintCanonicalConversions
+  | PrintUniverses of bool * string option
+  | PrintHint of reference or_by_notation
+  | PrintHintGoal
+  | PrintHintDbName of string
+  | PrintRewriteHintDbName of string
+  | PrintHintDb
+  | PrintScopes
+  | PrintScope of string
+  | PrintVisibility of string option
+  | PrintAbout of reference or_by_notation*int 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
+  | LocateTactic of reference
+  | LocateFile of string
+
+type showable =
+  | ShowGoal of goal_reference
+  | ShowGoalImplicitly of int option
+  | ShowProof
+  | ShowNode
+  | ShowScript
+  | ShowExistentials
+  | ShowUniverses
+  | ShowTree
+  | ShowProofNames
+  | ShowIntros of bool
+  | ShowMatch of lident
+  | ShowThesis
+
+type comment =
+  | CommentConstr of constr_expr
+  | CommentString of string
+  | CommentInt of int
+
+type reference_or_constr = 
+  | HintsReference of reference
+  | HintsConstr of constr_expr
+
+type hints_expr =
+  | HintsResolve of (int option * bool * reference_or_constr) list
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of reference list
+  | HintsTransparency of reference list * bool
+  | HintsMode of reference * bool list
+  | HintsConstructors of reference list
+  | HintsExtern of int * constr_expr option * raw_tactic_expr
+
+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   = bool (* true = Opaque;        false = 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 = Decl_kinds.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 obsolete_locality = bool
+(* Some grammar entries use obsolete_locality.  This bool is to be backward
+ * compatible.  If the grammar is fixed removing deprecated syntax, this
+ * bool should go away too *)
+
+type option_value = Goptions.option_value =
+  | BoolValue of bool
+  | IntValue of int option
+  | StringValue of string
+
+type option_ref_value =
+  | StringRefValue of string
+  | QualidRefValue of reference
+
+type sort_expr = glob_sort
+
+type definition_expr =
+  | ProveBody of local_binder list * constr_expr
+  | DefineBody of local_binder list * raw_red_expr option * constr_expr
+      * constr_expr option
+
+type fixpoint_expr =
+    Id.t located * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
+
+type cofixpoint_expr =
+    Id.t located * local_binder 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 =
+  lident with_coercion * local_binder list * constr_expr option * inductive_kind *
+    constructor_list_or_record_decl_expr
+
+type one_inductive_expr =
+  lident * local_binder list * constr_expr option * constructor_expr list
+
+type grammar_tactic_prod_item_expr =
+  | TacTerm of string
+  | TacNonTerm of Loc.t * string * (Names.Id.t * string) option
+
+type syntax_modifier =
+  | SetItemLevel of string list * Extend.production_level
+  | SetLevel of int
+  | SetAssoc of Extend.gram_assoc
+  | SetEntryType of string * Extend.simple_constr_prod_entry_key
+  | SetOnlyParsing of Flags.compat_version
+  | SetFormat of string * string located
+
+type proof_end =
+  | Admitted
+  | Proved of opacity_flag * (lident * theorem_kind option) 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 =
+  | SsSet of lident list
+  | SsCompl of section_subset_expr
+  | SsUnion of section_subset_expr * section_subset_expr
+  | SsSubstr of section_subset_expr * section_subset_expr
+
+type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr
+
+type extend_name = string * 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 Stm} *)
+type 'a stm_vernac =
+  | JoinDocument
+  | Finish
+  | Wait
+  | PrintDag
+  | Observe of Stateid.t
+  | Command of 'a (* An out of flow command not to be recorded by Stm *)
+  | PGLast of 'a (* To ease the life of PG *)
+
+(** {6 Types concerning the module layer} *)
+
+(** Rigid / flexible module signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Which module inline annotations should we honor,
+    either None or the ones whose level is less or equal
+    to the given integer *)
+
+type inline =
+  | NoInline
+  | DefaultInline
+  | InlineAt of int
+
+type module_ast_inl = module_ast * inline
+type module_binder = bool option * lident list * module_ast_inl
+
+(** {6 The type of vernacular expressions} *)
+
+type vernac_expr =
+  (* Control *)
+  | VernacLoad of verbose_flag * string
+  | VernacTime of vernac_list
+  | VernacTimeout of int * vernac_expr
+  | VernacFail of vernac_expr
+  | VernacError of exn (* always fails *)
+
+  (* Syntax *)
+  | VernacTacticNotation of
+      int * grammar_tactic_prod_item_expr list * raw_tactic_expr
+  | VernacSyntaxExtension of
+      obsolete_locality * (lstring * syntax_modifier list)
+  | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
+  | VernacDelimiters of scope_name * string
+  | VernacBindScope of scope_name * reference or_by_notation list
+  | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
+      constr_expr * scope_name option
+  | VernacNotation of
+      obsolete_locality * constr_expr * (lstring * syntax_modifier list) *
+      scope_name option
+  | VernacNotationAddFormat of string * string * string
+
+  (* Gallina *)
+  | VernacDefinition of
+      (locality option * definition_object_kind) * lident * definition_expr
+  | VernacStartTheoremProof of theorem_kind * 
+      (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list *
+        bool
+  | VernacEndProof of proof_end
+  | VernacExactProof of constr_expr
+  | VernacAssumption of (locality option * assumption_object_kind) *
+      inline * simple_binder with_coercion list
+  | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacFixpoint of
+      locality option * (fixpoint_expr * decl_notation list) list
+  | VernacCoFixpoint of
+      locality option * (cofixpoint_expr * decl_notation list) list
+  | VernacScheme of (lident option * scheme) list
+  | VernacCombinedScheme of lident * lident list
+  | VernacUniverse of lident list
+  | VernacConstraint of (lident * Univ.constraint_type * lident) list
+
+  (* Gallina extensions *)
+  | VernacBeginSection of lident
+  | VernacEndSegment of lident
+  | VernacRequire of
+      export_flag option * lreference list
+  | VernacImport of export_flag * lreference list
+  | VernacCanonical of reference or_by_notation
+  | VernacCoercion of obsolete_locality * reference or_by_notation *
+      class_rawexpr * class_rawexpr
+  | VernacIdentityCoercion of obsolete_locality * lident *
+      class_rawexpr * class_rawexpr
+  | VernacNameSectionHypSet of lident * section_subset_descr 
+
+  (* Type classes *)
+  | VernacInstance of
+      bool * (* abstract instance *)
+      local_binder list * (* super *)
+	typeclass_constraint * (* instance name, class name, params *)
+	(bool * constr_expr) option * (* props *)
+	int option (* Priority *)
+
+  | VernacContext of local_binder list
+
+  | VernacDeclareInstances of
+    reference list * int option (* instance names, priority *)
+
+  | 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 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 *)
+
+  | VernacSolve of goal_selector * int option * raw_tactic_expr * bool
+  | 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 *)
+  | VernacDeclareTacticDefinition of
+      (rec_flag * (reference * bool * raw_tactic_expr) list)
+  | VernacCreateHintDb of string * bool
+  | VernacRemoveHints of string list * reference list
+  | VernacHints of obsolete_locality * string list * hints_expr
+  | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) *
+      obsolete_locality * onlyparsing_flag
+  | VernacDeclareImplicits of reference or_by_notation *
+      (explicitation * bool * bool) list list
+  | VernacArguments of reference or_by_notation *
+      ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list *
+      int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
+              `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
+              `DefaultImplicits ] list
+  | VernacArgumentsScope of reference or_by_notation *
+      scope_name option 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 Goptions.option_name
+  | VernacSetOption of 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 raw_red_expr option * int option * constr_expr
+  | VernacGlobalCheck of constr_expr
+  | VernacDeclareReduction of string * raw_red_expr
+  | VernacPrint of printable
+  | VernacSearch of searchable * int option * search_restriction
+  | VernacLocate of locatable
+  | VernacRegister of lident * register_kind
+  | VernacComments of comment list
+  | VernacNop
+
+  (* Stm backdoor *)
+  | VernacStm of vernac_expr stm_vernac
+
+  (* Proof management *)
+  | VernacGoal of constr_expr
+  | VernacAbort of lident option
+  | VernacAbortAll
+  | VernacRestart
+  | VernacUndo of int
+  | VernacUndoTo of int
+  | VernacBacktrack of int*int*int
+  | VernacFocus of int option
+  | VernacUnfocus
+  | VernacUnfocused
+  | VernacBullet of bullet
+  | VernacSubproof of int option
+  | VernacEndSubproof
+  | VernacShow of showable
+  | VernacCheckGuard
+  | VernacProof of raw_tactic_expr option * section_subset_descr option
+  | VernacProofMode of string
+  (* Toplevel control *)
+  | VernacToplevelControl of exn
+
+  (* For extension *)
+  | VernacExtend of extend_name * Genarg.raw_generic_argument list
+
+  (* Flags *)
+  | VernacProgram of vernac_expr
+  | VernacPolymorphic of bool * vernac_expr
+  | VernacLocal of bool * vernac_expr
+
+and vernac_list = located_vernac_expr list
+
+and located_vernac_expr = Loc.t * vernac_expr
+
+(* A vernac classifier has to tell if a command:
+   vernac_when: has to be executed now (alters the parser) or later
+   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 *)
+type vernac_type =
+  | VtStartProof of vernac_start
+  | VtSideff of vernac_sideff_type
+  | VtQed of vernac_qed_type
+  | VtProofStep of bool (* parallelize *)
+  | VtProofMode of string
+  | VtQuery of vernac_part_of_script * report_with
+  | VtStm of vernac_control * vernac_part_of_script
+  | VtUnknown
+and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *)
+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 vernac_is_alias = bool
+and vernac_part_of_script = bool
+and vernac_control =
+  | VtFinish
+  | VtWait
+  | VtJoinDocument
+  | VtPrintDag
+  | VtObserve of Stateid.t
+  | VtBack of Stateid.t
+  | VtPG
+and opacity_guarantee =
+  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
+  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+type vernac_when =
+  | VtNow
+  | VtLater
+type vernac_classification = vernac_type * vernac_when