path: root/API/API.mli

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

module Prelude :
sig
  (* None of the items in this modules are meant to be used by plugin-writers.
     This module is here only for "technical reasons"
     (it will disappear when we take advantage of mutually-recursive modules) *)

  (* API.Term.constr *)
  type constr = Constr.t

  (* API.Term.types *)
  type types = Constr.t

  (* API.Evar.t *)
  type evar = Evar.t

  (* 'constr API.Term.pexistential *)
  type 'constr pexistential = evar * 'constr array

  (* API.Environ.env *)
  type env = Environ.env

  (* API.Evar.Map.t *)
  type evar_map = Evd.evar_map

  (* API.Globnames.global_reference *)
  type global_reference = Globnames.global_reference

  type rigid = Evd.rigid =
             | UnivRigid
             | UnivFlexible of bool

  type conv_pb = Reduction.conv_pb =
    | CONV
    | CUMUL

  type named_context_val = Environ.named_context_val

  type metavariable = int

  (* Termops.meta_value_map *)
  type meta_value_map = (metavariable * constr) list

  (* API.Libnames.reference *)
  type reference = Libnames.reference =
         | Qualid of Libnames.qualid Loc.located
         | Ident of Names.Id.t Loc.located
end

module Univ :
sig
  module Level :
  sig
    type t = Univ.Level.t
    val set : t
    val pr : t -> Pp.std_ppcmds
  end

  module Instance :
  sig 
    type t = Univ.Instance.t
    val empty : t
    val of_array : Level.t array -> t
    val to_array : t -> Level.t array
    val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
  end
  type 'a puniverses = 'a * Instance.t

  module Constraint : module type of struct include Univ.Constraint end

  type 'a constrained = 'a * Constraint.t

  module UContext :
  sig
    type t = Univ.UContext.t
    val empty : t
  end

  type universe_context = UContext.t
  [@@ocaml.deprecated "alias of API.Names.UContext.t"]

  type universe_info_ind = Univ.UInfoInd.t

  module LSet : module type of struct include Univ.LSet end
  module ContextSet : 
  sig
    type t = Univ.ContextSet.t
    val empty : t
    val of_context : UContext.t -> t
    val to_context : t -> UContext.t
  end

  type 'a in_universe_context_set = 'a * ContextSet.t
  type 'a in_universe_context = 'a * UContext.t
  type constraint_type = Univ.constraint_type

  module Universe :
  sig
    type t = Univ.Universe.t
    val pr : t -> Pp.std_ppcmds
  end

  type universe_context_set = ContextSet.t
  [@@ocaml.deprecated "alias of API.Names.ContextSet.t"]

  type universe_set = LSet.t
  [@@ocaml.deprecated "alias of API.Names.LSet.t"]

  type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t
  type universe_subst = Univ.universe_subst
  type universe_level_subst = Univ.universe_level_subst

  val enforce_leq : Universe.t constraint_function
  val pr_uni : Universe.t -> Pp.std_ppcmds
  val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> UContext.t -> Pp.std_ppcmds
  val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> ContextSet.t -> Pp.std_ppcmds
  val pr_universe_subst : universe_subst -> Pp.std_ppcmds
  val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds
  val pr_constraints : (Level.t -> Pp.std_ppcmds) -> Constraint.t -> Pp.std_ppcmds
end

module UState :
sig
  type t = UState.t
  val context : t -> Univ.UContext.t
  val context_set : t -> Univ.ContextSet.t
  val of_context_set : Univ.ContextSet.t -> t
end

module Sorts :
sig
  type contents = Sorts.contents = Pos | Null
  type t = Sorts.t =
         | Prop of contents
         | Type of Univ.Universe.t
  val is_prop : t -> bool
  val hash : t -> int

  type family = Sorts.family = InProp | InSet | InType
  val family : t -> family
end

module Names :
sig
  module Id : module type of struct include Names.Id end

  module MBId : sig
    type t = Names.MBId.t
    val equal : t -> t -> bool
    val to_id : t -> Names.Id.t
    val repr : t -> int * Names.Id.t * Names.DirPath.t    
    val debug_to_string : t -> string
  end

  type evaluable_global_reference = Names.evaluable_global_reference =
    | EvalVarRef of Id.t
    | EvalConstRef of Names.Constant.t

  module Name : module type of struct include Names.Name end

  type name = Name.t =
    | Anonymous     
    | Name of Id.t
  [@@ocaml.deprecated "alias of API.Name.t"]

  module DirPath :
  sig
    type t = Names.DirPath.t
    val empty : t
    val make : Id.t list -> t
    val repr : t -> Id.t list
    val equal : t -> t -> bool
    val to_string : t -> string
  end

  module Label :
  sig
    type t = Names.Label.t
    val make : string -> t
    val equal : t -> t -> bool
    val compare : t -> t -> int
    val of_id : Names.Id.t -> t
    val to_id : t -> Names.Id.t
    val to_string : t -> string
  end

  module ModPath :
  sig
    type t = Names.ModPath.t =
           | MPfile of Names.DirPath.t
           | MPbound of MBId.t
           | MPdot of t * Label.t
    val compare : t -> t -> int
    val equal : t -> t -> bool
    val hash : t -> int
    val initial : t
    val to_string : t -> string
    val debug_to_string : t -> string
  end

  module KerName :
  sig
    type t = Names.KerName.t
    val make : ModPath.t -> DirPath.t -> Label.t -> t
    val make2 : ModPath.t -> Label.t -> t
    val modpath : t -> ModPath.t
    val equal : t -> t -> bool
    val compare : t -> t -> int
    val label : t -> Label.t
    val repr : t -> ModPath.t * DirPath.t * Label.t
    val print : t -> Pp.std_ppcmds
    val to_string : t -> string
  end

  type kernel_name = KerName.t
  [@@ocaml.deprecated "alias of API.Names.KerName.t"]

  module Constant :
  sig
    type t = Names.Constant.t
    val equal : t -> t -> bool
    val make1 : Names.KerName.t -> t
    val make2 : Names.ModPath.t -> Label.t -> t
    val make3 : Names.ModPath.t -> Names.DirPath.t -> Label.t -> t
    val repr3 : t -> Names.ModPath.t * Names.DirPath.t * Label.t
    val canonical : t -> Names.KerName.t
    val user : t -> Names.KerName.t
    val label : t -> Label.t
  end

  module MutInd :
  sig
    type t = Names.MutInd.t
    val make1 : Names.KerName.t -> t
    val make2 : Names.ModPath.t -> Label.t -> t
    val equal : t -> t -> bool
    val repr3 : t -> Names.ModPath.t * Names.DirPath.t * Label.t
    val canonical : t -> Names.KerName.t
    val modpath : t -> Names.ModPath.t
    val label : t -> Label.t
    val user : t -> Names.KerName.t
    val print : t -> Pp.std_ppcmds
  end

  module Projection :
  sig
    type t = Names.Projection.t
    val make : Constant.t -> bool -> t
    val map : (Constant.t -> Constant.t) -> t -> t
    val constant : t -> Constant.t
    val equal : t -> t -> bool
  end

  type inductive = MutInd.t * int
  val eq_ind : inductive -> inductive -> bool

  type constructor = inductive * int
  val eq_constructor : constructor -> constructor -> bool
  val constructor_hash : constructor -> int

  module MPset : module type of struct include Names.MPset end
  module MPmap : module type of struct include Names.MPmap end
  module KNset : module type of struct include Names.KNset end
  module KNmap : module type of struct include Names.KNmap end
  module Cset : module type of struct include Names.Cset end
  module Cset_env : module type of struct include Names.Cset_env end
  module Cmap : module type of struct include Names.Cmap end
  module Cmap_env : module type of struct include Names.Cmap_env end
  module Cpred : module type of struct include  Names.Cpred end
  module Mindset : module type of struct include Names.Mindset end
  module Mindmap : module type of struct include Names.Mindmap end
  module Mindmap_env : module type of struct include Names.Mindmap_env end
  module Indmap : module type of struct include Names.Indmap end
                                   with type key = inductive
  module Indmap_env : module type of struct include Names.Indmap_env end
  module Constrmap : module type of struct include Names.Constrmap end
  module Constrmap_env : module type of struct include Names.Constrmap_env end

  type transparent_state = Id.Pred.t * Cpred.t
  val empty_transparent_state : transparent_state
  val full_transparent_state : transparent_state
  val var_full_transparent_state : transparent_state
  val cst_full_transparent_state : transparent_state

  val pr_kn : KerName.t -> Pp.std_ppcmds
  [@@ocaml.deprecated "alias of API.Names.KerName.print"]

  val eq_constant : Constant.t -> Constant.t -> bool
  [@@ocaml.deprecated "alias of API.Names.Constant.equal"]

  type module_path = ModPath.t =
    | MPfile of DirPath.t
    | MPbound of MBId.t
    | MPdot of ModPath.t * Label.t
  [@@ocaml.deprecated "alias of API.Names.ModPath.t"]

  type variable = Id.t
  [@@ocaml.deprecated "alias of API.Names.Id.t"]

  type 'a tableKey = 'a Names.tableKey =
    | ConstKey of 'a
    | VarKey of Id.t
    | RelKey of Int.t

  val id_of_string : string -> Id.t
  [@@ocaml.deprecated "alias of API.Names.Id.of_string"]

  val string_of_id : Id.t -> string
  [@@ocaml.deprecated "alias of API.Names.Id.to_string"]

  type mutual_inductive = MutInd.t
  [@@ocaml.deprecated "alias of API.Names.MutInd.t"]

  val eq_mind : MutInd.t -> MutInd.t -> bool
  [@@ocaml.deprecated "alias of API.Names.MutInd.equal"]

  val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t
  [@@ocaml.deprecated "alias of API.Names.Constant.repr3"]

  val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t
  [@@ocaml.deprecated "alias of API.Names.MutInd.repr3"]

  val initial_path : ModPath.t
  [@@ocaml.deprecated "alias of API.Names.ModPath.initial"]

  val con_label : Constant.t -> Label.t
  [@@ocaml.deprecated "alias of API.Names.Constant.label"]

  val mind_label : MutInd.t -> Label.t
  [@@ocaml.deprecated "alias of API.Names.MutInd.label"]

  val string_of_mp : ModPath.t -> string
  [@@ocaml.deprecated "alias of API.Names.ModPath.to_string"]

  val mind_of_kn : KerName.t -> MutInd.t
  [@@ocaml.deprecated "alias of API.Names.MutInd.make1"]

  type constant = Constant.t
  [@@ocaml.deprecated "alias of API.Names.Constant.t"]

  val mind_modpath : MutInd.t -> ModPath.t
  [@@ocaml.deprecated "alias of API.Names.MutInd.modpath"]

  val canonical_mind : MutInd.t -> KerName.t
  [@@ocaml.deprecated "alias of API.Names.MutInd.canonical"]

  val user_mind : MutInd.t -> KerName.t
  [@@ocaml.deprecated "alias of API.Names.MutInd.user"]

  val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t
  [@@ocaml.deprecated "alias of API.Names.KerName.repr"]

  val constant_of_kn : KerName.t -> Constant.t
  [@@ocaml.deprecated "alias of API.Names.Constant.make1"]

  val user_con : Constant.t -> KerName.t
  [@@ocaml.deprecated "alias of API.Names.Constant.user"]

  val modpath : KerName.t -> ModPath.t
  [@@ocaml.deprecated "alias of API.Names.KerName.modpath"]

  val canonical_con : Constant.t -> KerName.t
  [@@ocaml.deprecated "alias of API.Names.Constant.canonical"]

  val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t
  [@@ocaml.deprecated "alias of API.Names.KerName.make"]

  val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t
  [@@ocaml.deprecated "alias of API.Names.Constant.make3"]

  val debug_pr_con : Constant.t -> Pp.std_ppcmds

  val debug_pr_mind : MutInd.t -> Pp.std_ppcmds

  val pr_con : Constant.t -> Pp.std_ppcmds

  val string_of_con : Constant.t -> string

  val string_of_mind : MutInd.t -> string

  val debug_string_of_mind : MutInd.t -> string

  val debug_string_of_con : Constant.t -> string

  module Idset : module type of struct include Id.Set end
end

module Context :
sig

  module Rel :
  sig
    module Declaration :
    sig
      (* local declaration *)
      (* local declaration *)
      type ('constr, 'types) pt = ('constr, 'types) Context.Rel.Declaration.pt =
        | LocalAssum of Names.Name.t * 'types            (** name, type *)
        | LocalDef of Names.Name.t * 'constr * 'types    (** name, value, type *)

      type t = (Prelude.constr, Prelude.types) pt

      (** Return the name bound by a given declaration. *)
      val get_name : ('c, 't) pt -> Names.Name.t

      (** Return the type of the name bound by a given declaration. *)
      val get_type : ('c, 't) pt -> 't

      (** Set the name that is bound by a given declaration. *)
      val set_name : Names.Name.t -> ('c, 't) pt -> ('c, 't) pt

      (** Set the type of the bound variable in a given declaration. *)
      val set_type : 't -> ('c, 't) pt -> ('c, 't) pt

      (** Return [true] iff a given declaration is a local assumption. *)
      val is_local_assum : ('c, 't) pt -> bool

      (** Return [true] iff a given declaration is a local definition. *)
      val is_local_def : ('c, 't) pt -> bool

      (** Check whether the two given declarations are equal. *)
      val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool

      (** Map the name bound by a given declaration. *)
      val map_name : (Names.Name.t -> Names.Name.t) -> ('c, 't) pt -> ('c, 't) pt

      (** For local assumptions, this function returns the original local assumptions.
        For local definitions, this function maps the value in the local definition. *)
      val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt

      (** Map the type of the name bound by a given declaration. *)
      val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt

      (** Map all terms in a given declaration. *)
      val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt

      (** Perform a given action on all terms in a given declaration. *)
      val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit 

      (** Reduce all terms in a given declaration to a single value. *)
      val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a
    end

    (** Rel-context is represented as a list of declarations.
        Inner-most declarations are at the beginning of the list.
        Outer-most declarations are at the end of the list. *)
    type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
    type t = Declaration.t list

    (** empty rel-context *)
    val empty : ('c, 't) pt

    (** Return a new rel-context enriched by with a given inner-most declaration. *)
    val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt

    (** Return the number of {e local declarations} in a given context. *)
    val length : ('c, 't) pt -> int

    (** Check whether given two rel-contexts are equal. *)
    val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool

    (** Return the number of {e local assumptions} in a given rel-context. *)
    val nhyps : ('c, 't) pt -> int

    (** Return a declaration designated by a given de Bruijn index.
      @raise Not_found if the designated de Bruijn index outside the range. *)
    val lookup : int -> ('c, 't) pt -> ('c, 't) Declaration.pt

    (** Map all terms in a given rel-context. *)
    val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt

    (** Perform a given action on every declaration in a given rel-context. *)
    val iter : ('c -> unit) -> ('c, 'c) pt -> unit

    (** Reduce all terms in a given rel-context to a single value.
      Innermost declarations are processed first. *)
    val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a

    (** Reduce all terms in a given rel-context to a single value.
      Outermost declarations are processed first. *)
    val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a

    (** [extended_vect n Γ] does the same, returning instead an array. *)
    val to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array
  end
  module Named :
  sig
    module Declaration :
    sig
      (** local declaration *)
      type ('constr, 'types) pt = ('constr, 'types) Context.Named.Declaration.pt =
        | LocalAssum of Names.Id.t * 'types             (** identifier, type *)
        | LocalDef of Names.Id.t * 'constr * 'types     (** identifier, value, type *)

      type t = (Prelude.constr, Prelude.types) pt

      (** Return the identifier bound by a given declaration. *)
      val get_id : ('c, 't) pt -> Names.Id.t

      (** Return the type of the name bound by a given declaration. *)
      val get_type : ('c, 't) pt -> 't

      (** Set the identifier that is bound by a given declaration. *)
      val set_id : Names.Id.t -> ('c, 't) pt -> ('c, 't) pt

      (** Set the type of the bound variable in a given declaration. *)
      val set_type : 't -> ('c, 't) pt -> ('c, 't) pt

      (** Return [true] iff a given declaration is a local assumption. *)
      val is_local_assum : ('c, 't) pt -> bool

      (** Return [true] iff a given declaration is a local definition. *)
      val is_local_def : ('c, 't) pt -> bool

      (** Check whether any term in a given declaration satisfies a given predicate. *)
      val exists : ('c -> bool) -> ('c, 'c) pt -> bool

      (** Check whether all terms in a given declaration satisfy a given predicate. *)
      val for_all : ('c -> bool) -> ('c, 'c) pt -> bool

      (** Check whether the two given declarations are equal. *)
      val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool

      (** Map the identifier bound by a given declaration. *)
      val map_id : (Names.Id.t -> Names.Id.t) -> ('c, 't) pt -> ('c, 't) pt

      (** For local assumptions, this function returns the original local assumptions.
        For local definitions, this function maps the value in the local definition. *)
      val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt

      (** Map the type of the name bound by a given declaration. *)
      val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt

      (** Map all terms in a given declaration. *)
      val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt

      (** Perform a given action on all terms in a given declaration. *)
      val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit

      (** Reduce all terms in a given declaration to a single value. *)
      val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a

      val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt
    end
    (** Named-context is represented as a list of declarations.
      Inner-most declarations are at the beginning of the list.
      Outer-most declarations are at the end of the list. *)
    type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
    type t = Declaration.t list

    (** empty named-context *)
    val empty : ('c, 't) pt

    (** Return a new named-context enriched by with a given inner-most declaration. *)
    val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt

    (** Return the number of {e local declarations} in a given named-context. *)
    val length : ('c, 't) pt -> int

    (** Return a declaration designated by an identifier of the variable bound in that declaration.
      @raise Not_found if the designated identifier is not bound in a given named-context. *)
    val lookup : Names.Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt

    (** Check whether given two named-contexts are equal. *)
    val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool

    (** Map all terms in a given named-context. *)
    val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt

    (** Perform a given action on every declaration in a given named-context. *)
    val iter : ('c -> unit) -> ('c, 'c) pt -> unit

    (** Reduce all terms in a given named-context to a single value.
      Innermost declarations are processed first. *)
    val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a

    (** Reduce all terms in a given named-context to a single value.
      Outermost declarations are processed first. *)
    val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a

    (** Return the set of all identifiers bound in a given named-context. *)
    val to_vars : ('c, 't) pt -> Names.Id.Set.t

    (** [to_instance Ω] builds an instance [args] such
      that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local
      definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
      gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
    val to_instance : (Names.Id.t -> 'r) -> ('c, 't) pt -> 'r list
  end
end

module Term :
sig
  type sorts_family = Sorts.family = InProp | InSet | InType
  [@@deprecated "alias of API.Sorts.family"]

  type metavariable = Prelude.metavariable

  type contents = Sorts.contents = Pos | Null

  type sorts = Sorts.t =
    | Prop of contents
    | Type of Univ.Universe.t
  [@@ocaml.deprecated "alias of API.Sorts.t"]

  type constr = Prelude.constr
  type types = Prelude.types
  type ('constr, 'types) prec_declaration = Names.Name.t array * 'types array * 'constr array
  type 'constr pexistential = 'constr Prelude.pexistential
  type cast_kind = Term.cast_kind =
                 | VMcast
                 | NATIVEcast
                 | DEFAULTcast
                 | REVERTcast
  type 'a puniverses = 'a Univ.puniverses
  type pconstant = Names.Constant.t puniverses
  type pinductive = Names.inductive puniverses
  type pconstructor = Names.constructor puniverses
  type case_style = Term.case_style =
                  | LetStyle
                  | IfStyle
                  | LetPatternStyle
                  | MatchStyle
                  | RegularStyle
  type case_printing = Term.case_printing =
                         { ind_tags  : bool list;
                           cstr_tags : bool list array;
                           style     : case_style
                         }
  type case_info = Term.case_info =
                     { ci_ind         : Names.inductive;
                       ci_npar        : int;
                       ci_cstr_ndecls : int array;
                       ci_cstr_nargs  : int array;
                       ci_pp_info     : case_printing
                     }
  type ('constr, 'types) pfixpoint =
    (int array * int) * ('constr, 'types) prec_declaration
  type ('constr, 'types) pcofixpoint =
    int * ('constr, 'types) prec_declaration
  type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Term.kind_of_term =
     | Rel       of int
     | Var       of Names.Id.t
     | Meta      of metavariable
     | Evar      of 'constr pexistential
     | Sort      of 'sort
     | Cast      of 'constr * cast_kind * 'types
     | Prod      of Names.Name.t * 'types * 'types
     | Lambda    of Names.Name.t * 'types * 'constr
     | LetIn     of Names.Name.t * 'constr * 'types * 'constr
     | App       of 'constr * 'constr array
     | Const     of (Names.Constant.t * 'univs)
     | Ind       of (Names.inductive * 'univs)
     | Construct of (Names.constructor * 'univs)
     | Case      of case_info * 'constr * 'constr * 'constr array
     | Fix       of ('constr, 'types) pfixpoint
     | CoFix     of ('constr, 'types) pcofixpoint
     | Proj      of Names.Projection.t * 'constr
  type existential = Prelude.evar * constr array
  type rec_declaration = Names.Name.t array * constr array * constr array
  type fixpoint = (int array * int) * rec_declaration
  type cofixpoint = int * rec_declaration
  val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
  val applistc : constr -> constr list -> constr

  val applist : constr * constr list -> constr
  [@@ocaml.deprecated "(sort of an) alias of API.Term.applistc"]

  val mkArrow : types -> types -> constr
  val mkRel : int -> constr
  val mkVar : Names.Id.t -> constr

  val mkMeta : Prelude.metavariable -> constr

  val mkEvar : existential -> constr
  val mkSort : Sorts.t -> types
  val mkProp : types
  val mkSet  : types
  val mkType : Univ.Universe.t -> types
  val mkCast : constr * cast_kind * constr -> constr
  val mkProd : Names.Name.t * types * types -> types
  val mkLambda : Names.Name.t * types * constr -> constr
  val mkLetIn : Names.Name.t * constr * types * constr -> constr
  val mkApp : constr * constr array -> constr
  val mkConst : Names.Constant.t -> constr
  val mkProj : Names.Projection.t * constr -> constr
  val mkInd : Names.inductive -> constr
  val mkConstruct : Names.constructor -> constr
  val mkConstructU : Names.constructor puniverses -> constr
  val mkConstructUi : (pinductive * int) -> constr
  val mkCase : case_info * constr * constr * constr array -> constr
  val mkFix : fixpoint -> constr
  val mkCoFix : cofixpoint -> constr
  val mkNamedLambda : Names.Id.t -> types -> constr -> constr
  val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr
  val mkNamedProd : Names.Id.t -> types -> types -> types

  val decompose_app : constr -> constr * constr list
  val decompose_prod : constr -> (Names.Name.t*constr) list * constr
  val decompose_prod_n : int -> constr -> (Names.Name.t * constr) list * constr
  val decompose_prod_assum : types -> Context.Rel.t * types
  val decompose_lam : constr -> (Names.Name.t * constr) list * constr
  val decompose_lam_n : int -> constr -> (Names.Name.t * constr) list * constr
  val decompose_prod_n_assum : int -> types -> Context.Rel.t * types

  val compose_prod : (Names.Name.t * constr) list -> constr -> constr
  val compose_lam : (Names.Name.t * constr) list -> constr -> constr

  val destSort : constr -> Sorts.t
  val destVar : constr -> Names.Id.t
  val destApp : constr -> constr * constr array
  val destProd : types -> Names.Name.t * types * types
  val destLetIn : constr -> Names.Name.t * constr * types * constr
  val destEvar : constr -> existential
  val destRel : constr -> int
  val destConst : constr -> Names.Constant.t puniverses
  val destCast : constr -> constr * cast_kind * constr
  val destLambda : constr -> Names.Name.t * types * constr

  val isRel : constr -> bool
  val isVar  : constr -> bool
  val isEvar : constr -> bool
  val isLetIn : constr -> bool
  val isLambda : constr -> bool
  val isConst : constr -> bool
  val isEvar_or_Meta : constr -> bool
  val isCast : constr -> bool
  val isMeta : constr -> bool
  val isApp : constr -> bool

  val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a

  val eq_constr : constr -> constr -> bool

  val hash_constr : constr -> int
  val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
  val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
  val prod_applist : constr -> constr list -> constr
  exception DestKO
  val map_constr : (constr -> constr) -> constr -> constr

  val mkIndU : pinductive -> constr
  val mkConstU : pconstant -> constr
  val map_constr_with_binders :
    ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
  val iter_constr : (constr -> unit) -> constr -> unit

  (* Quotients away universes: really needed?
   * Can't we just call eq_c_univs_infer and discard the inferred csts?
   *)
  val eq_constr_nounivs : constr -> constr -> bool

  type ('constr, 'types) kind_of_type = ('constr, 'types) Term.kind_of_type =                                          
                                      | SortType   of Sorts.t
                                      | CastType   of 'types * 'types
                                      | ProdType   of Names.Name.t * 'types * 'types
                                      | LetInType  of Names.Name.t * 'constr * 'types * 'types
                                      | AtomicType of 'constr * 'constr array
  val kind_of_type : types -> (constr, types) kind_of_type

  val is_prop_sort : Sorts.t -> bool
  [@@ocaml.deprecated "alias of API.Sorts.is_prop"]

  type existential_key = Prelude.evar

  val family_of_sort : Sorts.t -> Sorts.family

  val compare : constr -> constr -> int

  val constr_ord : constr -> constr -> int
  [@@ocaml.deprecated "alias of API.Term.compare"]

  val destInd : constr -> Names.inductive puniverses
  val univ_of_sort : Sorts.t -> Univ.Universe.t

  val strip_lam : constr -> constr
  val strip_prod_assum : types -> types

  val decompose_lam_assum : constr -> Context.Rel.t * constr
  val destFix : constr -> fixpoint

  val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
end

module EConstr :
sig
  type t = EConstr.t
  type constr = t
  type types = t
  type unsafe_judgment = EConstr.unsafe_judgment
  type named_declaration = (constr, types) Context.Named.Declaration.pt
  type named_context = (constr, types) Context.Named.pt
  type rel_context = (constr, types) Context.Rel.pt
  type rel_declaration = (constr, types) Context.Rel.Declaration.pt
  type existential = constr Term.pexistential
  module ESorts :
  sig
    type t = EConstr.ESorts.t
    (** Type of sorts up-to universe unification. Essentially a wrapper around
      Sorts.t so that normalization is ensured statically. *)

    val make : Sorts.t -> t
    (** Turn a sort into an up-to sort. *)

    val kind : Prelude.evar_map -> t -> Sorts.t
    (** Returns the view into the current sort. Note that the kind of a variable
        may change if the unification state of the evar map changes. *)

  end
  
  module EInstance :
  sig
    type t = EConstr.EInstance.t
    (** Type of universe instances up-to universe unification. Similar to
      {ESorts.t} for {Univ.Instance.t}. *)

    val make : Univ.Instance.t -> t
    val kind : Prelude.evar_map -> t -> Univ.Instance.t
    val empty : t
    val is_empty : t -> bool
  end
    
  val of_constr : Term.constr -> constr

  val kind : Prelude.evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) Term.kind_of_term

  val mkArrow : constr -> constr -> constr
  val mkInd : Names.inductive -> t
  val mkProp : constr
  val mkProd : Names.Name.t * constr * constr -> constr
  val mkRel : int -> constr
  val mkSort : Sorts.t -> constr
  val mkVar : Names.Id.t -> constr
  val mkLambda : Names.Name.t * constr * constr -> constr
  val mkLambda_or_LetIn : rel_declaration -> constr -> constr
  val mkApp : constr * constr array -> constr
  val mkEvar : constr Term.pexistential -> constr

  val mkMeta : Prelude.metavariable -> constr

  val mkConstructU : Names.constructor * EInstance.t -> constr
  val mkLetIn : Names.Name.t * constr * constr * constr -> constr
  val mkProd_or_LetIn : rel_declaration -> constr -> constr
  val mkCast : constr * Term.cast_kind * constr -> constr
  val mkNamedLambda : Names.Id.t -> types -> constr -> constr
  val mkNamedProd : Names.Id.t -> types -> types -> types

  val isCast : Evd.evar_map -> t -> bool
  val isEvar : Prelude.evar_map -> constr -> bool
  val isInd  : Prelude.evar_map -> constr -> bool
  val isRel : Prelude.evar_map -> constr -> bool
  val isSort : Prelude.evar_map -> constr -> bool
  val isVar : Prelude.evar_map -> constr -> bool
  val isConst : Prelude.evar_map -> constr -> bool
  val isConstruct : Prelude.evar_map -> constr -> bool

  val destInd : Prelude.evar_map -> constr -> Names.inductive * EInstance.t
  val destVar : Prelude.evar_map -> constr -> Names.Id.t
  val destEvar : Prelude.evar_map -> constr -> constr Term.pexistential
  val destRel : Prelude.evar_map -> constr -> int
  val destProd : Prelude.evar_map -> constr -> Names.Name.t * types * types
  val destLambda : Prelude.evar_map -> constr -> Names.Name.t * types * constr
  val destApp : Prelude.evar_map -> constr -> constr * constr array
  val destConst : Prelude.evar_map -> constr -> Names.Constant.t * EInstance.t
  val destConstruct : Prelude.evar_map -> constr -> Names.constructor * EInstance.t
  val destFix : Evd.evar_map -> t -> (t, t) Term.pfixpoint
  val destCast : Evd.evar_map -> t -> t * Term.cast_kind * t

  val mkConstruct : Names.constructor -> constr

  val compose_lam : (Names.Name.t * constr) list -> constr -> constr

  val decompose_lam : Prelude.evar_map -> constr -> (Names.Name.t * constr) list * constr
  val decompose_lam_n_assum : Prelude.evar_map -> int -> constr -> rel_context * constr
  val decompose_app : Prelude.evar_map -> constr -> constr * constr list
  val decompose_prod : Prelude.evar_map -> constr -> (Names.Name.t * constr) list * constr
  val decompose_prod_assum : Prelude.evar_map -> constr -> rel_context * constr

  val applist : constr * constr list -> constr

  val to_constr : Prelude.evar_map -> constr -> Constr.t

  val push_rel : rel_declaration -> Prelude.env -> Prelude.env

  module Unsafe :
  sig
    val to_constr : constr -> Term.constr

    val to_rel_decl : (constr, types) Context.Rel.Declaration.pt -> (Prelude.constr, Prelude.types) Context.Rel.Declaration.pt

    (** Physical identity. Does not care for defined evars. *)

    val to_named_decl : (constr, types) Context.Named.Declaration.pt -> (Prelude.constr, Prelude.types) Context.Named.Declaration.pt

    val to_instance : EInstance.t -> Univ.Instance.t
  end

  module Vars :
  sig
    val substnl : t list -> int -> t -> t
    val noccurn : Prelude.evar_map -> int -> constr -> bool
    val closed0 : Prelude.evar_map -> constr -> bool
    val subst1 : constr -> constr -> constr
    val substl : constr list -> constr -> constr
    val lift : int -> constr -> constr
    val liftn : int -> int -> t -> t
    val subst_var : Names.Id.t -> t -> t
    val subst_vars : Names.Id.t list -> t -> t
  end

  val fresh_global :
    ?loc:Loc.t -> ?rigid:Prelude.rigid -> ?names:Univ.Instance.t -> Environ.env ->
    Evd.evar_map -> Prelude.global_reference -> Evd.evar_map * t

val of_named_decl : (Term.constr, Term.types) Context.Named.Declaration.pt -> (constr, types) Context.Named.Declaration.pt
  val of_rel_decl : (Term.constr, Term.types) Context.Rel.Declaration.pt -> (constr, types) Context.Rel.Declaration.pt
  val kind_of_type : Prelude.evar_map -> constr -> (constr, constr) Term.kind_of_type
  val to_lambda : Prelude.evar_map -> int -> constr -> constr
  val it_mkLambda_or_LetIn : constr -> rel_context -> constr
  val push_rel_context : rel_context -> Prelude.env -> Prelude.env
  val eq_constr : Prelude.evar_map -> constr -> constr -> bool
  val iter_with_binders : Prelude.evar_map -> ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
  val fold : Prelude.evar_map -> ('a -> constr -> 'a) -> 'a -> constr -> 'a
  val existential_type : Prelude.evar_map -> existential -> types
  val iter : Prelude.evar_map -> (constr -> unit) -> constr -> unit
  val eq_constr_universes : Prelude.evar_map -> constr -> constr -> Universes.universe_constraints option
  val eq_constr_nounivs : Prelude.evar_map -> constr -> constr -> bool
  val compare_constr : Evd.evar_map -> (constr -> constr -> bool) -> constr -> constr -> bool
  val isApp : Prelude.evar_map -> constr -> bool
  val it_mkProd_or_LetIn : constr -> rel_context -> constr
  val push_named : named_declaration -> Prelude.env -> Prelude.env
  val destCase : Prelude.evar_map -> constr -> Term.case_info * constr * constr * constr array
  val decompose_lam_assum : Prelude.evar_map -> constr -> rel_context * constr
  val mkConst : Names.Constant.t -> constr
  val mkCase : Term.case_info * constr * constr * constr array -> constr
  val named_context : Prelude.env -> named_context
  val val_of_named_context : named_context -> Prelude.named_context_val
  val mkFix : (t, t) Term.pfixpoint -> t
  val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t
  val isMeta : Evd.evar_map -> t -> bool

  val destMeta : Evd.evar_map -> t -> Term.metavariable

  val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
  val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr
  val map : Evd.evar_map -> (t -> t) -> t -> t
  val mkConstU : Names.Constant.t * EInstance.t -> t
  val isProd : Evd.evar_map -> t -> bool
  val mkConstructUi : (Names.inductive * EInstance.t) * int -> t
  val isLambda : Evd.evar_map -> t -> bool
end

module Mod_subst :
sig
  type substitution = Mod_subst.substitution
  type 'a substituted = 'a Mod_subst.substituted
  type delta_resolver = Mod_subst.delta_resolver

  val force_constr : Term.constr substituted -> Term.constr

  val empty_delta_resolver : delta_resolver
  val constant_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.Constant.t
  val mind_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.MutInd.t
  val subst_kn : substitution -> Names.KerName.t -> Names.KerName.t
  val subst_evaluable_reference :
    substitution -> Names.evaluable_global_reference -> Names.evaluable_global_reference
  val subst_mps : substitution -> Term.constr -> Term.constr
  val subst_constant : substitution -> Names.Constant.t -> Names.Constant.t
  val subst_ind : substitution -> Names.inductive -> Names.inductive
  val debug_pr_subst : substitution -> Pp.std_ppcmds
  val debug_pr_delta : delta_resolver -> Pp.std_ppcmds
end

module Retroknowledge :
sig
  type action = Retroknowledge.action
  type nat_field = Retroknowledge.nat_field =
    | NatType
    | NatPlus
    | NatTimes
  type n_field = Retroknowledge.n_field =
    | NPositive
    | NType
    | NTwice
    | NTwicePlusOne
    | NPhi
    | NPhiInv
    | NPlus
    | NTimes
  type int31_field = Retroknowledge.int31_field =
    | Int31Bits
    | Int31Type
    | Int31Constructor
    | Int31Twice
    | Int31TwicePlusOne
    | Int31Phi
    | Int31PhiInv
    | Int31Plus
    | Int31PlusC
    | Int31PlusCarryC
    | Int31Minus
    | Int31MinusC
    | Int31MinusCarryC
    | Int31Times
    | Int31TimesC
    | Int31Div21
    | Int31Div
    | Int31Diveucl
    | Int31AddMulDiv
    | Int31Compare
    | Int31Head0
    | Int31Tail0
    | Int31Lor
    | Int31Land
    | Int31Lxor
  type field = Retroknowledge.field =
    | KInt31 of string * int31_field
end

module Declarations :
sig
  type recarg = Declarations.recarg =
    | Norec
    | Mrec of Names.inductive
    | Imbr of Names.inductive
  type wf_paths = recarg Rtree.t
  type inline = Declarations.inline
  type constant_def = Declarations.constant_def =
                    | Undef of inline
                    | Def of Term.constr Mod_subst.substituted
                    | OpaqueDef of Opaqueproof.opaque
  type constant_type = Declarations.constant_type
  type constant_universes = Declarations.constant_universes
  type projection_body = Declarations.projection_body = {
        proj_ind : Names.MutInd.t;
        proj_npars : int;
        proj_arg : int;
        proj_type : Term.types;
        proj_eta : Term.constr * Term.types;
        proj_body : Term.constr;
      }
  type typing_flags = Declarations.typing_flags
  type constant_body = Declarations.constant_body = {
        const_hyps : Context.Named.t;
        const_body : constant_def;
        const_type : constant_type;
        const_body_code : Cemitcodes.to_patch_substituted option;
        const_polymorphic : bool;
        const_universes : constant_universes;
        const_proj : projection_body option;
        const_inline_code : bool;
        const_typing_flags : typing_flags;
      }
  type one_inductive_body = Declarations.one_inductive_body = {
        mind_typename : Names.Id.t;
        mind_arity_ctxt : Context.Rel.t;
        mind_arity : Declarations.inductive_arity;
        mind_consnames : Names.Id.t array;
        mind_user_lc : Term.types array;
        mind_nrealargs : int;
        mind_nrealdecls : int;
        mind_kelim : Sorts.family list;
        mind_nf_lc : Term.types array;
        mind_consnrealargs : int array;
        mind_consnrealdecls : int array;
        mind_recargs : wf_paths;
        mind_nb_constant : int;
        mind_nb_args : int;
        mind_reloc_tbl :  Cbytecodes.reloc_table;
      }
  type ('ty,'a) functorize = ('ty,'a) Declarations.functorize =
                           | NoFunctor of 'a
                           | MoreFunctor of Names.MBId.t * 'ty * ('ty,'a) functorize
  type with_declaration = Declarations.with_declaration =
                        | WithMod of Names.Id.t list * Names.ModPath.t
                        | WithDef of Names.Id.t list * Term.constr Univ.in_universe_context
  type module_alg_expr = Declarations.module_alg_expr =
                       | MEident of Names.ModPath.t
                       | MEapply of module_alg_expr * Names.ModPath.t
                       | MEwith of module_alg_expr * with_declaration
  type mutual_inductive_body = Declarations.mutual_inductive_body = {
        mind_packets : one_inductive_body array;
        mind_record : Declarations.record_body option;
        mind_finite : Decl_kinds.recursivity_kind;
        mind_ntypes : int;
        mind_hyps : Context.Named.t;
        mind_nparams : int;
        mind_nparams_rec : int;
        mind_params_ctxt : Context.Rel.t;
        mind_polymorphic : bool;
        mind_universes : Univ.universe_info_ind;
        mind_private : bool option;
        mind_typing_flags : Declarations.typing_flags;
      }
   and module_expression = (module_type_body,module_alg_expr) functorize
   and module_implementation = Declarations.module_implementation =
                             | Abstract
                               | Algebraic of module_expression
                             | Struct of module_signature
                             | FullStruct
   and module_body = Declarations.module_body =
                       { mod_mp : Names.ModPath.t;
                         mod_expr : module_implementation;
                         mod_type : module_signature;
                         mod_type_alg : module_expression option;
                         mod_constraints : Univ.ContextSet.t;
                         mod_delta : Mod_subst.delta_resolver;
                         mod_retroknowledge : Retroknowledge.action list
                       }
   and module_signature = (module_type_body,structure_body) functorize
   and module_type_body = module_body
   and structure_body = (Names.Label.t * structure_field_body) list
   and structure_field_body = Declarations.structure_field_body =
                            | SFBconst of constant_body
                            | SFBmind of mutual_inductive_body
                            | SFBmodule of module_body
                            | SFBmodtype of module_type_body
end

module Univops : sig
  val universes_of_constr : Term.constr -> Univ.LSet.t
  val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
end

module Environ :
sig
  type env = Prelude.env
  type named_context_val = Prelude.named_context_val
  type ('constr, 'types) punsafe_judgment = ('constr, 'types) Environ.punsafe_judgment =
    {
      uj_val : 'constr;
      uj_type : 'types
    }
  val empty_env : env
  val lookup_mind : Names.MutInd.t -> env -> Declarations.mutual_inductive_body
  val push_rel : Context.Rel.Declaration.t -> env -> env
  val push_rel_context : Context.Rel.t -> env -> env
  val push_rec_types : Term.rec_declaration -> env -> env
  val lookup_rel : int -> env -> Context.Rel.Declaration.t
  val lookup_named : Names.Id.t -> env -> Context.Named.Declaration.t
  val lookup_named_val : Names.Id.t -> Environ.named_context_val -> Context.Named.Declaration.t
  val lookup_constant : Names.Constant.t -> env -> Declarations.constant_body
  val opaque_tables : env -> Opaqueproof.opaquetab
  val is_projection : Names.Constant.t -> env -> bool
  val lookup_projection : Names.Projection.t -> env -> Declarations.projection_body
  val named_context_of_val : named_context_val -> Context.Named.t
  val push_named : Context.Named.Declaration.t -> env -> env
  val named_context : env -> Context.Named.t
  val named_context_val : env -> named_context_val
  val push_named_context_val : Context.Named.Declaration.t -> named_context_val -> named_context_val
  val reset_with_named_context : named_context_val -> env -> env
  val rel_context : env -> Context.Rel.t
  val constant_value_in : env -> Names.Constant.t Univ.puniverses -> Term.constr
  val named_type : Names.Id.t -> env -> Term.types
  val constant_opt_value_in : env -> Names.Constant.t Univ.puniverses -> Term.constr option
  val fold_named_context_reverse :
    ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
  val evaluable_named  : Names.Id.t -> Environ.env -> bool
end

module UGraph :
sig
  type t = UGraph.t
  val pr_universes : (Univ.Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
end

module Reduction :
sig
  exception NotConvertible
  type conv_pb = Prelude.conv_pb =
               | CONV
               | CUMUL

  val whd_all : Environ.env -> Term.constr -> Term.constr

  val whd_betaiotazeta : Environ.env -> Term.constr -> Term.constr

  val is_arity : Environ.env -> Term.types -> bool

  val dest_prod : Environ.env -> Term.types -> Context.Rel.t * Term.types

  type 'a extended_conversion_function = 
    ?l2r:bool -> ?reds:Names.transparent_state -> Environ.env ->
    ?evars:((Term.existential->Term.constr option) * UGraph.t) ->
    'a -> 'a -> unit
  val conv : Term.constr extended_conversion_function
end

module Vars :
sig
  type substl = Term.constr list

  val substl : substl -> Term.constr -> Term.constr

  val subst1 : Term.constr -> Term.constr -> Term.constr

  val lift : int -> Term.constr -> Term.constr

  val closed0 : Term.constr -> bool

  val closedn : int -> Term.constr -> bool

  val replace_vars : (Names.Id.t * Term.constr) list -> Term.constr -> Term.constr

  val noccurn : int -> Term.constr -> bool
  val subst_var : Names.Id.t -> Term.constr -> Term.constr
  val subst_vars : Names.Id.t list -> Term.constr -> Term.constr
  val substnl : substl -> int -> Term.constr -> Term.constr
end

module Inductive :
sig
  type mind_specif = Declarations.mutual_inductive_body * Declarations.one_inductive_body
  val type_of_inductive : Environ.env -> mind_specif Univ.puniverses -> Term.types
  exception SingletonInductiveBecomesProp of Names.Id.t
  val lookup_mind_specif : Environ.env -> Names.inductive -> mind_specif
  val find_inductive  : Environ.env -> Term.types -> Term.pinductive * Term.constr list
end

module Typeops :
sig
  val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types
  val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types
end

module Opaqueproof :
sig
  type opaquetab = Opaqueproof.opaquetab
  type opaque = Opaqueproof.opaque
  val empty_opaquetab : opaquetab
  val force_proof : opaquetab -> opaque -> Term.constr
end

module Modops :
sig
  val destr_nofunctor : ('ty,'a) Declarations.functorize -> 'a
  val add_structure :
    Names.ModPath.t -> Declarations.structure_body -> Mod_subst.delta_resolver ->
    Environ.env -> Environ.env
  val add_module_type : Names.ModPath.t -> Declarations.module_type_body -> Environ.env -> Environ.env
end

module Entries :
sig
  type mutual_inductive_entry = Entries.mutual_inductive_entry
  type inline = int option
  type 'a proof_output = Term.constr Univ.in_universe_context_set * 'a
  type 'a const_entry_body = 'a proof_output Future.computation
  type 'a definition_entry = 'a Entries.definition_entry =
                               { const_entry_body   : 'a const_entry_body;
                                 (* List of section variables *)
                                 const_entry_secctx : Context.Named.t option;
                                 (* State id on which the completion of type checking is reported *)
                                 const_entry_feedback : Stateid.t option;
                                 const_entry_type        : Term.types option;
                                 const_entry_polymorphic : bool;
                                 const_entry_universes   : Univ.UContext.t;
                                 const_entry_opaque      : bool;
                                 const_entry_inline_code : bool }
  type parameter_entry = Context.Named.t option * bool * Term.types Univ.in_universe_context * inline 
  type projection_entry = Entries.projection_entry
  type 'a constant_entry = 'a Entries.constant_entry =
                         | DefinitionEntry of 'a definition_entry
                         | ParameterEntry of parameter_entry
                         | ProjectionEntry of projection_entry
end

module Mod_typing :
sig
  type 'alg translation =
    Declarations.module_signature * 'alg * Mod_subst.delta_resolver * Univ.ContextSet.t
  val translate_mse :
    Environ.env -> Names.ModPath.t option -> Entries.inline -> Declarations.module_alg_expr ->
    Declarations.module_alg_expr translation
end

module Esubst :
sig
  type 'a subs = 'a Esubst.subs
  val subs_id : int -> 'a subs
end

module CClosure :
sig
  type fconstr = CClosure.fconstr
  type clos_infos = CClosure.clos_infos
  type table_key = Names.Constant.t Univ.puniverses Names.tableKey
  type fterm = CClosure.fterm =
    | FRel of int
    | FAtom of Term.constr (** Metas and Sorts *)
    | FCast of fconstr * Term.cast_kind * fconstr
    | FFlex of table_key
    | FInd of Names.inductive Univ.puniverses
    | FConstruct of Names.constructor Univ.puniverses
    | FApp of fconstr * fconstr array
    | FProj of Names.Projection.t * fconstr
    | FFix of Term.fixpoint * fconstr Esubst.subs
    | FCoFix of Term.cofixpoint * fconstr Esubst.subs
    | FCaseT of Term.case_info * Term.constr * fconstr * Term.constr array * fconstr Esubst.subs (* predicate and branches are closures *)
    | FLambda of int * (Names.Name.t * Term.constr) list * Term.constr * fconstr Esubst.subs
    | FProd of Names.Name.t * fconstr * fconstr
    | FLetIn of Names.Name.t * fconstr * fconstr * Term.constr * fconstr Esubst.subs
    | FEvar of Term.existential * fconstr Esubst.subs
    | FLIFT of int * fconstr
    | FCLOS of Term.constr * fconstr Esubst.subs
    | FLOCKED
  module RedFlags : sig
    type reds = CClosure.RedFlags.reds
    type red_kind = CClosure.RedFlags.red_kind
    val mkflags : red_kind list -> reds
    val fBETA : red_kind
    val fCOFIX : red_kind
    val fCONST : Names.Constant.t -> CClosure.RedFlags.red_kind
    val fFIX : red_kind
    val fMATCH : red_kind
    val fZETA : red_kind
    val red_add_transparent : reds -> Names.transparent_state -> reds
  end
  val mk_clos : fconstr Esubst.subs -> Term.constr -> fconstr
  val mk_atom : Term.constr -> fconstr
  val mk_clos_deep :
    (fconstr Esubst.subs -> Term.constr -> fconstr) ->
    fconstr Esubst.subs -> Term.constr -> fconstr
  val mk_red : fterm -> fconstr
  val all : RedFlags.reds
  val beta : RedFlags.reds
  val betaiota : RedFlags.reds
  val betaiotazeta : RedFlags.reds

  val create_clos_infos : ?evars:(Term.existential -> Term.constr option) -> RedFlags.reds -> Environ.env -> clos_infos

  val whd_val : clos_infos -> fconstr -> Term.constr

  val inject : Term.constr -> fconstr

  val kl : clos_infos -> fconstr -> Term.constr
  val term_of_fconstr : fconstr -> Term.constr
end

module Type_errors :
sig
  type type_error = Type_errors.type_error
  exception TypeError of Environ.env * type_error
end

module Evar :
sig
  (** Unique identifier of some {i evar} *)
  type t = Prelude.evar

  (** Recover the underlying integer. *)
  val repr : t -> int

  val equal : t -> t -> bool

  (** a set of unique identifiers of some {i evars} *)
  module Set : module type of struct include Evar.Set end
end

module Evd :
sig
  val string_of_existential : Evar.t -> string
  type evar_constraint = Prelude.conv_pb * Environ.env * Term.constr * Term.constr

  (* --------------------------------- *)

  (* evar info *)

  module Store :
  sig
    type t = Evd.Store.t
    val empty : t
  end

  module Filter :
  sig
    type t = Evd.Filter.t
    val repr : t -> bool list option
  end

  (** This value defines the refinement of a given {i evar} *)
  type evar_body = Evd.evar_body =
              | Evar_empty (** given {i evar} was not yet refined *)
              | Evar_defined of Term.constr (** given {i var} was refined to the indicated term *)

  (** all the information we have concerning some {i evar} *)
  type evar_info = Evd.evar_info =
    {
      evar_concl : Term.constr;
      evar_hyps : Environ.named_context_val;
      evar_body : evar_body;
      evar_filter : Filter.t;
      evar_source : Evar_kinds.t Loc.located;
      evar_candidates : Term.constr list option; (* if not None, list of allowed instances *)
      evar_extra : Store.t
    }

  val evar_concl : evar_info -> Term.constr
  val evar_body : evar_info -> evar_body
  val evar_context : evar_info -> Context.Named.t
  val instantiate_evar_array : evar_info -> Term.constr -> Term.constr array -> Term.constr
  val evar_filtered_env : evar_info -> Environ.env
  val evar_hyps : evar_info -> Environ.named_context_val

  (* ------------------------------------ *)

  (* evar map *)

  type evar_map = Prelude.evar_map
  type open_constr = evar_map * Term.constr

  type rigid = Prelude.rigid =
    | UnivRigid
      | UnivFlexible of bool

                          
    type 'a freelisted = 'a Evd.freelisted = {
          rebus : 'a;
          freemetas : Evd.Metaset.t
        }
    type instance_status = Evd.instance_status
    type clbinding = Evd.clbinding =
      | Cltyp of Names.Name.t * Term.constr freelisted
      | Clval of Names.Name.t * (Term.constr freelisted * instance_status) * Term.constr freelisted
    val empty : evar_map
    val from_env : Environ.env -> evar_map
    val find : evar_map -> Evar.t -> evar_info
    val find_undefined : evar_map -> Prelude.evar -> evar_info
    val is_defined : evar_map -> Evar.t -> bool
    val mem : evar_map -> Evar.t -> bool
    val add : evar_map -> Evar.t -> evar_info -> evar_map
    val evar_universe_context : evar_map -> UState.t
    val set_universe_context : evar_map -> UState.t -> evar_map
    val universes : evar_map -> UGraph.t
    val define : Evar.t -> Term.constr -> evar_map -> evar_map
    val fold : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
    val evar_key : Names.Id.t -> evar_map -> Evar.t

    val create_evar_defs : evar_map -> evar_map

    val meta_declare : Prelude.metavariable -> Term.types -> ?name:Names.Name.t -> evar_map -> evar_map

    val clear_metas : evar_map -> evar_map

    (** Allocates a new evar that represents a {i sort}. *)
    val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t

    val remove : evar_map -> Evar.t -> evar_map
    val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> Environ.env ->
                       evar_map -> Prelude.global_reference -> evar_map * Term.constr
    val evar_filtered_context : evar_info -> Context.Named.t
    val fresh_inductive_instance : ?loc:Loc.t -> Environ.env -> evar_map -> Names.inductive -> evar_map * Term.pinductive
    val fold_undefined : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a

    val universe_context_set : evar_map -> Univ.ContextSet.t
    val evar_ident : Prelude.evar -> evar_map -> Names.Id.t option
    val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
    val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map ->
                           (Names.Id.t * Univ.Level.t) list * Univ.UContext.t
    val nf_constraints : evar_map -> evar_map
    val from_ctx : UState.t -> evar_map

    val meta_list : evar_map -> (Prelude.metavariable * clbinding) list

    val meta_defined : evar_map -> Prelude.metavariable -> bool

    val meta_name : evar_map -> Prelude.metavariable -> Names.Name.t

    module MonadR :
    sig
      module List :
      sig
        val map_right : ('a -> evar_map -> evar_map * 'b) -> 'a list -> evar_map -> evar_map * 'b list
      end
    end

  type 'a sigma = 'a Evd.sigma = {
        it : 'a ;
        sigma : evar_map
      }

  val sig_sig : 'a sigma -> evar_map

  val sig_it  : 'a sigma -> 'a

  type 'a in_evar_universe_context = 'a * UState.t

  val univ_flexible : rigid
  val univ_flexible_alg : rigid
  val empty_evar_universe_context : UState.t
  val union_evar_universe_context : UState.t -> UState.t -> UState.t
  val merge_universe_context : evar_map -> UState.t -> evar_map

  type unsolvability_explanation = Evd.unsolvability_explanation =
                                 | SeveralInstancesFound of int
    
  module Metaset : module type of struct include Evd.Metaset end
                                  with type elt = Prelude.metavariable

  (** Return {i ids} of all {i evars} that occur in a given term. *)
  val evars_of_term : Term.constr -> Evar.Set.t

  val evar_universe_context_of : Univ.ContextSet.t -> UState.t
  [@@ocaml.deprecated "alias of API.UState.of_context_set"]

  val evar_context_universe_context : UState.t -> Univ.UContext.t
  [@@ocaml.deprecated "alias of API.UState.context"]

  type evar_universe_context = UState.t
  [@@ocaml.deprecated "alias of API.UState.t"]

  val existential_opt_value : evar_map -> Term.existential -> Term.constr option
  val existential_value : evar_map -> Term.existential -> Term.constr

  exception NotInstantiatedEvar

  val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> Environ.env -> evar_map -> Sorts.family -> evar_map * Sorts.t
end

module Namegen :
sig
  (** *)

  (** [next_ident_away original_id unwanted_ids] returns a new identifier as close as possible
      to the [original_id] while avoiding all [unwanted_ids].

      In particular:
      {ul {- if [original_id] does not appear in the list of [unwanted_ids], then [original_id] is returned.}
          {- if [original_id] appears in the list of [unwanted_ids],
             then this function returns a new id that:
             {ul {- has the same {i root} as the [original_id],}
                 {- does not occur in the list of [unwanted_ids],}
                 {- has the smallest possible {i subscript}.}}}}

      where by {i subscript} of some identifier we mean last part of it that is composed
      only from (decimal) digits and by {i root} of some identifier we mean
      the whole identifier except for the {i subscript}.

      E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *)
  val next_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t

  val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string
  val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t
  val next_ident_away_in_goal : Names.Id.t -> Names.Id.t list -> Names.Id.t
  val default_dependent_ident : Names.Id.t
  val next_global_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t
  val rename_bound_vars_as_displayed :
    Evd.evar_map -> Names.Id.t list -> Names.Name.t list -> EConstr.types -> EConstr.types
end

module Safe_typing :
sig
  type private_constants = Safe_typing.private_constants
  val mk_pure_proof : Term.constr -> Safe_typing.private_constants Entries.proof_output
end

module Proofview_monad :
sig
  type lazy_msg = unit -> Pp.std_ppcmds
  module Info :
  sig
    type tree = Proofview_monad.Info.tree
  end
end

(* All items in the Goal modules are deprecated. *)
module Goal :
sig
  type goal = Evar.t

  val pr_goal : goal -> Pp.std_ppcmds

  module V82 :
  sig
    val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma

    val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val

    val env : Evd.evar_map -> goal -> Environ.env

    val concl : Evd.evar_map -> goal -> EConstr.constr

    val mk_goal : Evd.evar_map ->
                  Environ.named_context_val ->
                  EConstr.constr ->
                  Evd.Store.t ->
                  goal * EConstr.constr * Evd.evar_map

    val extra : Evd.evar_map -> goal -> Evd.Store.t

    val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map

    val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map

    val hyps : Evd.evar_map -> goal -> Environ.named_context_val

    val abstract_type : Evd.evar_map -> goal -> EConstr.types
  end
end

module Proofview :
sig
  type proofview = Proofview.proofview
  type entry = Proofview.entry
  type +'a tactic = 'a Proofview.tactic
  type telescope = Proofview.telescope =
    | TNil of Evd.evar_map
    | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
  module NonLogical :
  sig
    type +'a t = 'a Proofview.NonLogical.t
    val make : (unit -> 'a) -> 'a t
    val return : 'a -> 'a t
    val ( >> ) : unit t -> 'a t -> 'a t
    val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
    val print_char : char -> unit t
    val print_debug : Pp.std_ppcmds -> unit t
    val print_warning : Pp.std_ppcmds -> unit t
    val print_notice : Pp.std_ppcmds -> unit t
    val print_info : Pp.std_ppcmds -> unit t
    val run : 'a t -> 'a
    type 'a ref = 'a Proofview.NonLogical.ref
    val ref : 'a -> 'a ref t
    val ( := ) : 'a ref -> 'a -> unit t
    val ( ! ) : 'a ref -> 'a t
    val raise : ?info:Exninfo.info -> exn -> 'a t
    val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
    val read_line : string t
  end
  val proofview : proofview -> Goal.goal list * Evd.evar_map
  val cycle : int -> unit tactic
  val swap : int -> int -> unit tactic
  val revgoals : unit tactic
  val give_up : unit tactic
  val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview
  val shelve : unit tactic
  val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
  val tclUNIT : 'a -> 'a tactic
  val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
  val tclORELSE : 'a tactic -> (Util.iexn -> 'a tactic) -> 'a tactic
  val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
  val tclEVARMAP : Evd.evar_map tactic
  val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
  val tclLIFT : 'a NonLogical.t -> 'a tactic
  val tclOR : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
  val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic
  val tclINDEPENDENT : unit tactic -> unit tactic
  val tclDISPATCH : unit tactic list -> unit tactic
  val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
  val tclBREAK : (Exninfo.iexn -> Exninfo.iexn option) -> 'a tactic -> 'a tactic
  val tclENV : Environ.env tactic
  val tclONCE : 'a tactic -> 'a tactic
  val tclPROGRESS : 'a tactic -> 'a tactic
  val shelve_unifiable : unit tactic
  val apply : Environ.env -> 'a tactic -> proofview -> 'a
                                                     * proofview
                                                     * (bool*Goal.goal list*Goal.goal list)
                                                     * Proofview_monad.Info.tree
  val numgoals : int tactic
  val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic

  module Unsafe :
  sig
    val tclEVARS : Evd.evar_map -> unit tactic

    val tclGETGOALS : Goal.goal list tactic

    val tclSETGOALS : Goal.goal list -> unit tactic

    val tclNEWGOALS : Goal.goal list -> unit tactic
  end

  module Goal :
  sig
    type 'a t = 'a Proofview.Goal.t
    val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
    val hyps : 'a t -> EConstr.named_context
    val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
    val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic
    val concl : 'a t -> EConstr.constr
    val sigma : 'a t -> Evd.evar_map
    val goal : [ `NF ] t -> Evar.t
    val env : 'a t -> Environ.env
    val assume : 'a t -> [ `NF ] t
  end

  module Notations :
  sig
    val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
    val (<*>) : unit tactic -> 'a tactic -> 'a tactic
    val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
  end
  module V82 :
  sig
    type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma

    val tactic : tac -> unit tactic

    val of_tactic : 'a tactic -> tac

    val nf_evar_goals : unit tactic

    val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic

    val catchable_exception : exn -> bool
  end
  module Trace :
  sig
    val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
    val log : Proofview_monad.lazy_msg -> unit tactic
  end
end

module Ftactic :
sig
  type +'a focus = 'a Ftactic.focus
  type +'a t = 'a focus Proofview.tactic
  val return : 'a -> 'a t
  val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
  val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
  val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
  val lift : 'a Proofview.tactic -> 'a t
  val with_env : 'a t -> (Environ.env * 'a) t
  module List :
  sig
    val map : ('a -> 'b t) -> 'a list -> 'b list t
    val map_right : ('a -> 'b t) -> 'a list -> 'b list t
  end
  module Notations :
  sig
    val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
    val (<*>) : unit t -> 'a t -> 'a t
  end
end

module Evarutil :
sig
  val e_new_global : Evd.evar_map ref -> Globnames.global_reference -> EConstr.constr

  val nf_evars_and_universes : Evd.evar_map -> Evd.evar_map * (Term.constr -> Term.constr)
  val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
  val nf_evar_info : Evd.evar_map -> Evd.evar_info -> Evd.evar_info

  val mk_new_meta : unit -> EConstr.constr

  (** [new_meta] is a generator of unique meta variables *)
  val new_meta : unit -> Prelude.metavariable

  val new_Type : ?rigid:Evd.rigid -> Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.constr
  val new_global : Evd.evar_map -> Prelude.global_reference -> Evd.evar_map * EConstr.constr

  val new_evar :
    Environ.env -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t ->
    ?candidates:EConstr.constr list -> ?store:Evd.Store.t ->
    ?naming:Misctypes.intro_pattern_naming_expr ->
    ?principal:bool -> EConstr.types -> Evd.evar_map * EConstr.constr

  val new_evar_instance :
    Environ.named_context_val -> Evd.evar_map -> EConstr.types -> 
    ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list ->
    ?store:Evd.Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
    ?principal:bool ->
    EConstr.constr list -> Evd.evar_map * EConstr.constr

  val clear_hyps_in_evi : Environ.env -> Evd.evar_map ref -> Environ.named_context_val ->
                          EConstr.types -> Names.Id.Set.t -> Environ.named_context_val * EConstr.types

  exception ClearDependencyError of Names.Id.t * Evarutil.clear_dependency_error
  val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t
  val e_new_evar :
      Environ.env -> Evd.evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t ->
      ?candidates:EConstr.constr list -> ?store:Evd.Store.t ->
      ?naming:Misctypes.intro_pattern_naming_expr ->
      ?principal:bool -> EConstr.types -> EConstr.constr
  val new_type_evar :
    Environ.env -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t ->
    ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> Evd.rigid ->
    Evd.evar_map * (EConstr.constr * Sorts.t)
  val nf_evars_universes : Evd.evar_map -> Term.constr -> Term.constr
  val safe_evar_value : Evd.evar_map -> Term.existential -> Term.constr option
  val evd_comb1 : (Evd.evar_map -> 'b -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'b -> 'a
end

module Geninterp :
sig
  module Val :
  sig
    type 'a typ = 'a Geninterp.Val.typ
    type t = Geninterp.Val.t = Dyn : 'a typ * 'a -> t
    type 'a tag = 'a Geninterp.Val.tag =
                | Base : 'a typ -> 'a tag
                | List : 'a tag -> 'a list tag
                | Opt : 'a tag -> 'a option tag
                | Pair : 'a tag * 'b tag -> ('a * 'b) tag
    val create : string -> 'a typ
    val pr : 'a typ -> Pp.std_ppcmds
    val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
    val typ_list : t list typ
    val typ_opt : t option typ
    val typ_pair : (t * t) typ
    val repr : 'a typ -> string
    val inject : 'a tag -> 'a -> t
  end
  module TacStore :
  sig
    type t = Geninterp.TacStore.t
    type 'a field = 'a Geninterp.TacStore.field
    val empty : t
    val field : unit -> 'a field
    val get : t -> 'a field -> 'a option
    val set : t -> 'a field -> 'a -> t
    val remove : t -> 'a field -> t
    val merge : t -> t -> t
  end
  type interp_sign = Geninterp.interp_sign =
                       {lfun : Val.t Names.Id.Map.t;
                        extra : TacStore.t }
  type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
  val register_interp0 :
    ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun -> unit
  val register_val0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'top Val.tag option -> unit
  val val_tag : 'a Genarg.typed_abstract_argument_type -> 'a Val.tag
  val interp : ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun
end

module Globnames :
sig
  type global_reference = Globnames.global_reference =
    | VarRef of Names.Id.t
    | ConstRef of Names.Constant.t
    | IndRef of Names.inductive
    | ConstructRef of Names.constructor

  type extended_global_reference = Globnames.extended_global_reference =
                                 | TrueGlobal of global_reference
                                 | SynDef of Names.KerName.t

  (* Long term: change implementation so that only 1 kind of order is needed.
   * Today: _env ones are fine grained, which one to pick depends.  Eg.
   *   - conversion rule are implemented by the non_env ones
   *   - pretty printing (of user provided names/aliases) are implemented by
   *     the _env ones
   *)
  module Refset : module type of struct include Globnames.Refset end
  module Refmap : module type of struct include Globnames.Refmap end
  module Refset_env : module type of struct include Globnames.Refset_env end
  module Refmap_env : module type of struct include Globnames.Refmap_env end
  module RefOrdered :
  sig
    type t = global_reference
    val compare : t -> t -> int
  end

  val pop_global_reference : global_reference -> global_reference
  val eq_gr : global_reference -> global_reference -> bool
  val destIndRef : global_reference -> Names.inductive

  val encode_mind : Names.DirPath.t -> Names.Id.t -> Names.MutInd.t
  val encode_con : Names.DirPath.t -> Names.Id.t -> Names.Constant.t

  val global_of_constr : Term.constr -> global_reference

  val subst_global : Mod_subst.substitution -> global_reference -> global_reference * Term.constr
  val destConstructRef : Globnames.global_reference -> Names.constructor

  val reference_of_constr : Term.constr -> global_reference
  [@@ocaml.deprecated "alias of API.Globnames.global_of_constr"]

  val is_global : global_reference -> Term.constr -> bool
end

module Evar_kinds :
sig
  type obligation_definition_status = Evar_kinds.obligation_definition_status =
                                    | Define of bool
                                    | Expand

  type matching_var_kind = Evar_kinds.matching_var_kind =
    | FirstOrderPatVar of Names.Id.t
    | SecondOrderPatVar of Names.Id.t

  type t = Evar_kinds.t =
         | ImplicitArg of Globnames.global_reference * (int * Names.Id.t option)
                          * bool (** Force inference *)
         | BinderType of Names.Name.t
         | NamedHole of Names.Id.t (* coming from some ?[id] syntax *)
         | QuestionMark of obligation_definition_status * Names.Name.t
         | CasesType of bool (* true = a subterm of the type *)
         | InternalHole
         | TomatchTypeParameter of Names.inductive * int
         | GoalEvar
         | ImpossibleCase
         | MatchingVar of matching_var_kind
         | VarInstance of Names.Id.t
         | SubEvar of Prelude.evar
end

module Decl_kinds :
sig
  type polymorphic = bool
  type recursivity_kind = Decl_kinds.recursivity_kind =
    | Finite
    | CoFinite
    | BiFinite
  type locality = Decl_kinds.locality =
    | Discharge
    | Local
    | Global
  type definition_object_kind = Decl_kinds.definition_object_kind =
    | Definition
    | Coercion
    | SubClass
    | CanonicalStructure
    | Example
    | Fixpoint
    | CoFixpoint
    | Scheme
    | StructureComponent
    | IdentityCoercion
    | Instance
    | Method
  type theorem_kind = Decl_kinds.theorem_kind =
    | Theorem
    | Lemma
    | Fact
    | Remark
    | Property
    | Proposition
    | Corollary
  type goal_object_kind = Decl_kinds.goal_object_kind =
    | DefinitionBody of definition_object_kind
    | Proof of theorem_kind
  type goal_kind = locality * polymorphic * goal_object_kind
  type assumption_object_kind = Decl_kinds.assumption_object_kind =
    | Definitional
    | Logical
    | Conjectural
  type logical_kind = Decl_kinds.logical_kind =
    | IsAssumption of assumption_object_kind
    | IsDefinition of definition_object_kind
    | IsProof of theorem_kind
  type binding_kind = Decl_kinds.binding_kind =
    | Explicit
    | Implicit
  type private_flag = bool
  type definition_kind = locality * polymorphic * definition_object_kind
end

module Misctypes :
sig
  type evars_flag = bool
  type clear_flag = bool option
  type advanced_flag = bool
  type rec_flag = bool

  type 'a or_by_notation = 'a Misctypes.or_by_notation =
    | AN of 'a
    | ByNotation of (string * string option) Loc.located
  type 'a or_var = 'a Misctypes.or_var =
                 | ArgArg of 'a
                 | ArgVar of Names.Id.t Loc.located
  type 'a and_short_name = 'a * Names.Id.t Loc.located option
  type glob_level = Misctypes.glob_level
  type 'a glob_sort_gen = 'a Misctypes.glob_sort_gen =
    | GProp
    | GSet
    | GType of 'a
  type sort_info = Names.Name.t Loc.located list
  type glob_sort = sort_info glob_sort_gen
  type 'a cast_type = 'a Misctypes.cast_type =
                    | CastConv of 'a
                    | CastVM of 'a
                    | CastCoerce
                    | CastNative of 'a
  type 'constr intro_pattern_expr = 'constr Misctypes.intro_pattern_expr =
    | IntroForthcoming of bool
    | IntroNaming of intro_pattern_naming_expr
    | IntroAction of 'constr intro_pattern_action_expr
   and intro_pattern_naming_expr = Misctypes.intro_pattern_naming_expr =
     | IntroIdentifier of Names.Id.t
     | IntroFresh of Names.Id.t
     | IntroAnonymous
   and 'constr intro_pattern_action_expr = 'constr Misctypes.intro_pattern_action_expr =
     | IntroWildcard
     | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
     | IntroInjection of ('constr intro_pattern_expr) Loc.located list
     | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located
     | IntroRewrite of bool
   and 'constr or_and_intro_pattern_expr = 'constr Misctypes.or_and_intro_pattern_expr =
     | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list
     | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list
  type quantified_hypothesis = Misctypes.quantified_hypothesis =
    | AnonHyp of int
    | NamedHyp of Names.Id.t
  type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list
  type 'a bindings = 'a Misctypes.bindings =
    | ImplicitBindings of 'a list
    | ExplicitBindings of 'a explicit_bindings
    | NoBindings
  type 'a with_bindings = 'a * 'a bindings
  type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
    | ElimOnConstr of 'a
    | ElimOnIdent of Names.Id.t Loc.located
    | ElimOnAnonHyp of int
  type inversion_kind = Misctypes.inversion_kind =
    | SimpleInversion
    | FullInversion
    | FullInversionClear
  type multi = Misctypes.multi =
    | Precisely of int
    | UpTo of int
    | RepeatStar
    | RepeatPlus
  type 'id move_location = 'id Misctypes.move_location =
    | MoveAfter of 'id
    | MoveBefore of 'id
    | MoveFirst
    | MoveLast
  type 'a destruction_arg = clear_flag * 'a core_destruction_arg
end

module Pattern :
sig
  type case_info_pattern = Pattern.case_info_pattern
  type constr_pattern = Pattern.constr_pattern =
    | PRef of Globnames.global_reference
    | PVar of Names.Id.t
    | PEvar of Evar.t * constr_pattern array
    | PRel of int
    | PApp of constr_pattern * constr_pattern array
    | PSoApp of Names.Id.t * constr_pattern list
    | PProj of Names.Projection.t * constr_pattern
    | PLambda of Names.Name.t * constr_pattern * constr_pattern
    | PProd of Names.Name.t * constr_pattern * constr_pattern
    | PLetIn of Names.Name.t * constr_pattern * constr_pattern option * constr_pattern
    | PSort of Misctypes.glob_sort
    | PMeta of Names.Id.t 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 Term.fixpoint
    | PCoFix of Term.cofixpoint
  type constr_under_binders = Names.Id.t list * EConstr.constr
  type extended_patvar_map = constr_under_binders Names.Id.Map.t
  type patvar_map = EConstr.constr Names.Id.Map.t
end

module Constrexpr :
sig
  type binder_kind = Constrexpr.binder_kind =
                   | Default of Decl_kinds.binding_kind
                   | Generalized of Decl_kinds.binding_kind * Decl_kinds.binding_kind * bool
  type explicitation = Constrexpr.explicitation =
                     | ExplByPos of int * Names.Id.t option
                     | ExplByName of Names.Id.t
  type sign = bool
  type raw_natural_number = string
  type prim_token = Constrexpr.prim_token =
                  | Numeral of raw_natural_number * sign
                  | String of string
  type notation = string
  type instance_expr = Misctypes.glob_level list
  type proj_flag = int option
  type abstraction_kind = Constrexpr.abstraction_kind =
                        | AbsLambda
                        | AbsPi
  type cases_pattern_expr_r = Constrexpr.cases_pattern_expr_r =
    | CPatAlias of cases_pattern_expr * Names.Id.t
    | CPatCstr  of Prelude.reference
      * cases_pattern_expr list option * cases_pattern_expr list
    (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
    | CPatAtom of Prelude.reference option
    | CPatOr   of cases_pattern_expr list
    | CPatNotation of notation * cases_pattern_notation_substitution
                      * cases_pattern_expr list
    | CPatPrim   of prim_token
    | CPatRecord of (Prelude.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 * cases_pattern_expr list list

   and constr_expr_r = Constrexpr.constr_expr_r =
     | CRef     of Prelude.reference * instance_expr option
     | CFix     of Names.Id.t Loc.located * fix_expr list
     | CCoFix   of Names.Id.t Loc.located * cofix_expr list
     | CProdN   of binder_expr list * constr_expr
     | CLambdaN of binder_expr list * constr_expr
     | CLetIn   of Names.Name.t Loc.located * constr_expr * constr_expr option * constr_expr
     | CAppExpl of (proj_flag * Prelude.reference * instance_expr option) * constr_expr list
     | CApp     of (proj_flag * constr_expr) *
                   (constr_expr * explicitation Loc.located option) list
     | CRecord  of (Prelude.reference * constr_expr) list
     | CCases of Term.case_style
               * constr_expr option
               * case_expr list
               * branch_expr list
     | CLetTuple of Names.Name.t Loc.located list * (Names.Name.t Loc.located option * constr_expr option) *
                    constr_expr * constr_expr
     | CIf of constr_expr * (Names.Name.t Loc.located option * constr_expr option)
            * constr_expr * constr_expr
     | CHole   of Evar_kinds.t option * Misctypes.intro_pattern_naming_expr * Genarg.raw_generic_argument option
     | CPatVar of Names.Id.t
     | CEvar   of Glob_term.existential_name * (Names.Id.t * constr_expr) list
     | CSort   of Misctypes.glob_sort
     | CCast   of constr_expr * constr_expr Misctypes.cast_type
     | CNotation of notation * constr_notation_substitution
     | CGeneralization of Decl_kinds.binding_kind * abstraction_kind option * constr_expr
     | CPrim of prim_token
     | CDelimiters of string * constr_expr
   and constr_expr = constr_expr_r CAst.t

   and case_expr = constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option

   and branch_expr =
     (cases_pattern_expr list Loc.located list * constr_expr) Loc.located

   and binder_expr =
     Names.Name.t Loc.located list * binder_kind * constr_expr

   and fix_expr =
     Names.Id.t Loc.located * (Names.Id.t Loc.located option * recursion_order_expr) *
       local_binder_expr list * constr_expr * constr_expr

   and cofix_expr =
     Names.Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr

   and recursion_order_expr = Constrexpr.recursion_order_expr =
                            | CStructRec
                              | CWfRec of constr_expr
                            | CMeasureRec of constr_expr * constr_expr option

   and local_binder_expr = Constrexpr.local_binder_expr =
     | CLocalAssum   of Names.Name.t Loc.located list * binder_kind * constr_expr
     | CLocalDef     of Names.Name.t Loc.located * constr_expr * constr_expr option
     | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located

   and constr_notation_substitution =
     constr_expr list *
       constr_expr list list *
         local_binder_expr list list

  type typeclass_constraint = (Names.Name.t Loc.located * Names.Id.t Loc.located list option) * Decl_kinds.binding_kind * constr_expr
  type constr_pattern_expr = constr_expr
end

module Goptions :
sig
  type option_name = string list
  type 'a option_sig = 'a Goptions.option_sig =
    {
      optdepr  : bool;
      optname  : string;
      optkey   : option_name;
      optread  : unit -> 'a;
      optwrite : 'a -> unit
    }
  type 'a write_function = 'a Goptions.write_function
  val declare_bool_option  : ?preprocess:(bool -> bool) ->
                             bool option_sig   -> bool write_function
  val declare_int_option   : ?preprocess:(int option -> int option) ->
                             int option option_sig -> int option write_function
  val declare_string_option: ?preprocess:(string -> string) ->
                             string option_sig -> string write_function
  val set_bool_option_value : option_name -> bool -> unit
end

module Locus :
sig
  type 'a occurrences_gen = 'a Locus.occurrences_gen =
  | AllOccurrences
  | AllOccurrencesBut of 'a list (** non-empty *)
  | NoOccurrences
  | OnlyOccurrences of 'a list (** non-empty *)
  type occurrences = int occurrences_gen
  type occurrences_expr = (int Misctypes.or_var) occurrences_gen
  type 'a with_occurrences = occurrences_expr * 'a
  type hyp_location_flag = Locus.hyp_location_flag =
                             InHyp | InHypTypeOnly | InHypValueOnly
  type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
  type 'id clause_expr = 'id Locus.clause_expr =
  { onhyps : 'id hyp_location_expr list option;
    concl_occs : occurrences_expr }
  type clause = Names.Id.t clause_expr
  type hyp_location = Names.Id.t * hyp_location_flag
  type goal_location = hyp_location option
end

module Genredexpr :
sig

  (** The parsing produces initially a list of [red_atom] *)

  type 'a red_atom = 'a Genredexpr.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 = 'a Genredexpr.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 = ('a,'b,'c) Genredexpr.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 = ('a,'b,'c) Genredexpr.may_eval =
    | ConstrTerm of 'a
    | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
    | ConstrContext of Names.Id.t Loc.located * 'a
    | ConstrTypeOf of 'a

  type r_trm = Constrexpr.constr_expr
  type r_pat = Constrexpr.constr_pattern_expr
  type r_cst = Prelude.reference Misctypes.or_by_notation
  type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
end

module Vernacexpr :
sig
  type instance_flag  = bool option
  type coercion_flag = bool
  type inductive_flag = Decl_kinds.recursivity_kind
  type lname = Names.Name.t Loc.located
  type lident = Names.Id.t Loc.located
  type opacity_flag = Vernacexpr.opacity_flag =
                    | Opaque of lident list option
                    | Transparent
  type locality_flag = bool
  type inductive_kind = Vernacexpr.inductive_kind =
    | Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool
  type 'a hint_info_gen = 'a Vernacexpr.hint_info_gen =
    { hint_priority : int option;
      hint_pattern : 'a option }
  type vernac_type = Vernacexpr.vernac_type =
                   | VtStartProof of vernac_start
                   | VtSideff of vernac_sideff_type
                   | VtQed of vernac_qed_type
                   | VtProofStep of proof_step
                   | 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
   and vernac_qed_type = Vernacexpr.vernac_qed_type =
                       | VtKeep
                         | VtKeepAsAxiom
                         | VtDrop
   and vernac_start = string * opacity_guarantee * Names.Id.t list
   and vernac_sideff_type = Names.Id.t list
   and vernac_part_of_script = bool
   and vernac_control = Vernacexpr.vernac_control =
                      | VtWait
                        | VtJoinDocument
                        | VtBack of Stateid.t
   and opacity_guarantee = Vernacexpr.opacity_guarantee =
                         | GuaranteesOpacity
                           | Doesn'tGuaranteeOpacity
   and proof_step = Vernacexpr.proof_step = {
         parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
         proof_block_detection : proof_block_name option
       }
   and solving_tac = bool
   and anon_abstracting_tac = bool
   and proof_block_name = string
  type vernac_when = Vernacexpr.vernac_when = 
                   | VtNow
                   | VtLater
  type verbose_flag = bool

  type obsolete_locality = bool

  type lstring = Vernacexpr.lstring
  type 'a with_coercion = coercion_flag * 'a
  type scope_name = string
  type decl_notation = lstring * Constrexpr.constr_expr * scope_name option
  type constructor_expr = (lident * Constrexpr.constr_expr) with_coercion
  type 'a with_notation = 'a * decl_notation list
  type local_decl_expr = Vernacexpr.local_decl_expr =
    | AssumExpr of lname * Constrexpr.constr_expr
    | DefExpr of lname * Constrexpr.constr_expr * Constrexpr.constr_expr option
  type 'a with_priority = 'a * int option
  type 'a with_instance = instance_flag * 'a
  type constructor_list_or_record_decl_expr = Vernacexpr.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 plident = lident * lident list option
  type inductive_expr = plident with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr

  type syntax_modifier = Vernacexpr.syntax_modifier
  type class_rawexpr = Vernacexpr.class_rawexpr
  type definition_expr = Vernacexpr.definition_expr
  type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
  type proof_expr = Vernacexpr.proof_expr
  type proof_end = Vernacexpr.proof_end =
    | Admitted
    | Proved of opacity_flag * lident option
  type inline = Vernacexpr.inline
  type fixpoint_expr = plident * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option
  type cofixpoint_expr = Vernacexpr.cofixpoint_expr
  type scheme = Vernacexpr.scheme
  type section_subset_expr = Vernacexpr.section_subset_expr
  type module_binder = Vernacexpr.module_binder
  type vernac_argument_status = Vernacexpr.vernac_argument_status
  type vernac_implicit_status = Vernacexpr.vernac_implicit_status
  type module_ast_inl = Vernacexpr.module_ast_inl
  type 'a module_signature = 'a Vernacexpr.module_signature
  type extend_name = string * int
  type simple_binder = Vernacexpr.simple_binder
  type option_value = Vernacexpr.option_value
  type showable = Vernacexpr.showable
  type bullet = Vernacexpr.bullet
  type stm_vernac = Vernacexpr.stm_vernac
  type comment = Vernacexpr.comment
  type register_kind = Vernacexpr.register_kind
  type locatable = Vernacexpr.locatable
  type search_restriction = Vernacexpr.search_restriction
  type searchable = Vernacexpr.searchable
  type printable = Vernacexpr.printable
  type option_ref_value = Vernacexpr.option_ref_value
  type onlyparsing_flag = Vernacexpr.onlyparsing_flag
  type reference_or_constr = Vernacexpr.reference_or_constr
  type hint_mode = Vernacexpr.hint_mode
  type hints_expr = Vernacexpr.hints_expr =
    | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
    | HintsImmediate of reference_or_constr list
    | HintsUnfold of Prelude.reference list
    | HintsTransparency of Prelude.reference list * bool
    | HintsMode of Prelude.reference * hint_mode list
    | HintsConstructors of Prelude.reference list
    | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
  type vernac_expr = Vernacexpr.vernac_expr =
  | VernacLoad of verbose_flag * string
  | VernacTime of vernac_expr Loc.located
  | VernacRedirect of string * vernac_expr Loc.located
  | VernacTimeout of int * vernac_expr
  | VernacFail of vernac_expr
  | VernacSyntaxExtension of
      obsolete_locality * (lstring * syntax_modifier list)
  | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
  | VernacDelimiters of scope_name * string option
  | VernacBindScope of scope_name * class_rawexpr list
  | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
      Constrexpr.constr_expr * scope_name option
  | VernacNotation of
      obsolete_locality * Constrexpr.constr_expr * (lstring * syntax_modifier list) *
      scope_name option
  | VernacNotationAddFormat of string * string * string
  | VernacDefinition of
      (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * plident * definition_expr
  | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list * bool
  | VernacEndProof of proof_end
  | VernacExactProof of Constrexpr.constr_expr
  | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
      inline * (plident list * Constrexpr.constr_expr) with_coercion list
  | VernacInductive of Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
  | VernacFixpoint of
      Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
  | VernacCoFixpoint of
      Decl_kinds.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 (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list
  | VernacBeginSection of lident
  | VernacEndSegment of lident
  | VernacRequire of
      Prelude.reference option * bool option * Prelude.reference list
  | VernacImport of bool * Prelude.reference list
  | VernacCanonical of Prelude.reference Misctypes.or_by_notation
  | VernacCoercion of obsolete_locality * Prelude.reference Misctypes.or_by_notation *
      class_rawexpr * class_rawexpr
  | VernacIdentityCoercion of obsolete_locality * lident *
      class_rawexpr * class_rawexpr
  | VernacNameSectionHypSet of lident * section_subset_expr
  | VernacInstance of
      bool *
      Constrexpr.local_binder_expr list *
        Constrexpr.typeclass_constraint *
          (bool * Constrexpr.constr_expr) option *
            hint_info_expr
  | VernacContext of Constrexpr.local_binder_expr list
  | VernacDeclareInstances of
    (Prelude.reference * hint_info_expr) list
  | VernacDeclareClass of Prelude.reference
  | 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
  | VernacSolveExistential of int * Constrexpr.constr_expr
  | VernacAddLoadPath of bool * string * Names.DirPath.t option
  | VernacRemoveLoadPath of string
  | VernacAddMLPath of bool * string
  | VernacDeclareMLModule of string list
  | VernacChdir of string option
  | VernacWriteState of string
  | VernacRestoreState of string
  | VernacResetName of lident
  | VernacResetInitial
  | VernacBack of int
  | VernacBackTo of int
  | VernacCreateHintDb of string * bool
  | VernacRemoveHints of string list * Prelude.reference list
  | VernacHints of obsolete_locality * string list * hints_expr
  | VernacSyntacticDefinition of Names.Id.t Loc.located * (Names.Id.t list * Constrexpr.constr_expr) *
      obsolete_locality * onlyparsing_flag
  | VernacDeclareImplicits of Prelude.reference Misctypes.or_by_notation *
                                (Constrexpr.explicitation * bool * bool) list list
  | VernacArguments of Prelude.reference Misctypes.or_by_notation *
      vernac_argument_status list *
        (Names.Name.t * vernac_implicit_status) list list *
      int option *
        [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
          `DefaultImplicits ] list
  | VernacArgumentsScope of Prelude.reference Misctypes.or_by_notation *
      scope_name option list
  | VernacReserve of simple_binder list
  | VernacGeneralizable of (lident list) option
  | VernacSetOpacity of (Conv_oracle.level * Prelude.reference Misctypes.or_by_notation list)
  | VernacSetStrategy of
      (Conv_oracle.level * Prelude.reference Misctypes.or_by_notation list) list
  | VernacUnsetOption of Goptions.option_name
  | VernacSetOption of Goptions.option_name * option_value
  | VernacSetAppendOption of Goptions.option_name * string
  | 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 * Constrexpr.constr_expr
  | VernacGlobalCheck of Constrexpr.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
  | VernacStm of stm_vernac
  | VernacGoal of Constrexpr.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 Genarg.raw_generic_argument option * section_subset_expr option
  | VernacProofMode of string
  | VernacToplevelControl of exn
  | VernacExtend of extend_name * Genarg.raw_generic_argument list
  | VernacProgram of vernac_expr
  | VernacPolymorphic of bool * vernac_expr
  | VernacLocal of bool * vernac_expr
  and goal_selector = Vernacexpr.goal_selector =
    | SelectNth of int
    | SelectList of (int * int) list
    | SelectId of Names.Id.t
    | SelectAll
  and vernac_classification = vernac_type * vernac_when
  and one_inductive_expr =
    plident * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list
end

module Glob_term :
sig
  type cases_pattern_r = Glob_term.cases_pattern_r =
    | PatVar  of Names.Name.t
    | PatCstr of Names.constructor * cases_pattern list * Names.Name.t
  and cases_pattern = cases_pattern_r CAst.t
  type existential_name = Names.Id.t
  type glob_constr_r = Glob_term.glob_constr_r =
    | GRef of Globnames.global_reference * Misctypes.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 Names.Id.t
        (** An identifier that cannot be regarded as "GRef".
            Bound variables are typically represented this way. *)
    | GEvar   of existential_name * (Names.Id.t * glob_constr) list
    | GPatVar of Evar_kinds.matching_var_kind
    | GApp    of glob_constr * glob_constr list
    | GLambda of Names.Name.t * Decl_kinds.binding_kind *  glob_constr * glob_constr
    | GProd   of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr
    | GLetIn  of Names.Name.t * glob_constr * glob_constr option * glob_constr
    | GCases  of Term.case_style * glob_constr option * tomatch_tuples * cases_clauses
    | GLetTuple of Names.Name.t list * (Names.Name.t * glob_constr option) * glob_constr * glob_constr
    | GIf   of glob_constr * (Names.Name.t * glob_constr option) * glob_constr * glob_constr
    | GRec  of fix_kind * Names.Id.t array * glob_decl list array *
               glob_constr array * glob_constr array
    | GSort of Misctypes.glob_sort
    | GHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
    | GCast of glob_constr * glob_constr Misctypes.cast_type

   and glob_constr = glob_constr_r CAst.t
   
   and glob_decl = Names.Name.t * Decl_kinds.binding_kind * glob_constr option * glob_constr
   
   and fix_recursion_order = Glob_term.fix_recursion_order =
                           | GStructRec
                             | GWfRec of glob_constr
                           | GMeasureRec of glob_constr * glob_constr option

   and fix_kind = Glob_term.fix_kind =
                | GFix of ((int option * fix_recursion_order) array * int)
                | GCoFix of int

   and predicate_pattern =
     Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located option

   and tomatch_tuple = (glob_constr * predicate_pattern)

   and tomatch_tuples = tomatch_tuple list

   and cases_clause = (Names.Id.t list * cases_pattern list * glob_constr) Loc.located
   and cases_clauses = cases_clause list

  type closure = Glob_term.closure =
    { idents:Names.Id.t Names.Id.Map.t;
      typed: Pattern.constr_under_binders Names.Id.Map.t ;
      untyped:closed_glob_constr Names.Id.Map.t }
   and closed_glob_constr = Glob_term.closed_glob_constr = {
       closure: closure;
       term: glob_constr }

  type var_map = Pattern.constr_under_binders Names.Id.Map.t
  type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t
  type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t
  type ltac_var_map = Glob_term.ltac_var_map = {
        ltac_constrs : var_map;
        (** Ltac variables bound to constrs *)
        ltac_uconstrs : uconstr_var_map;
        (** Ltac variables bound to untyped constrs *)
        ltac_idents: Names.Id.t Names.Id.Map.t;
        (** Ltac variables bound to identifiers *)
        ltac_genargs : unbound_ltac_var_map;
        (** Ltac variables bound to other kinds of arguments *)
      }
end

module Libnames :
sig
  type full_path = Libnames.full_path
  val pr_path : Libnames.full_path -> Pp.std_ppcmds
  val make_path : Names.DirPath.t -> Names.Id.t -> full_path
  val eq_full_path : full_path -> full_path -> bool
  val dirpath : full_path -> Names.DirPath.t
  val path_of_string : string -> full_path

  type qualid = Libnames.qualid
  val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid
  val qualid_eq : qualid -> qualid -> bool
  val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t
  val pr_qualid : qualid -> Pp.std_ppcmds
  val string_of_qualid : qualid -> string
  val qualid_of_string : string -> qualid
  val qualid_of_path : full_path -> qualid
  val qualid_of_dirpath : Names.DirPath.t -> qualid
  val qualid_of_ident : Names.Id.t -> qualid

  type reference = Prelude.reference =
    | Qualid of Libnames.qualid Loc.located
    | Ident of Names.Id.t Loc.located
  val loc_of_reference : reference -> Loc.t option
  val qualid_of_reference : reference -> qualid Loc.located
  val pr_reference : reference -> Pp.std_ppcmds

  val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool
  val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t
  val dirpath_of_string : string -> Names.DirPath.t
  val pr_dirpath : Names.DirPath.t -> Pp.std_ppcmds

  val string_of_path : full_path -> string
  val basename : full_path -> Names.Id.t

  type object_name = Libnames.full_path * Names.KerName.t
  type object_prefix = Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t)

  module Dirset : module type of struct include Libnames.Dirset end
  module Dirmap : module type of struct include  Libnames.Dirmap end
  module Spmap : module type of struct include Libnames.Spmap end
end

module Libobject :
sig
  type obj = Libobject.obj
  type 'a substitutivity = 'a Libobject.substitutivity =
                         | Dispose
                           | Substitute of 'a
                         | Keep of 'a
                         | Anticipate of 'a
  type 'a object_declaration = 'a Libobject.object_declaration =
                                 {
                                   object_name : string;
                                   cache_function : Libnames.object_name * 'a -> unit;
                                   load_function : int -> Libnames.object_name * 'a -> unit;
                                   open_function : int -> Libnames.object_name * 'a -> unit;
                                   classify_function : 'a -> 'a substitutivity;
                                   subst_function :  Mod_subst.substitution * 'a -> 'a;
                                   discharge_function : Libnames.object_name * 'a -> 'a option;
                                   rebuild_function : 'a -> 'a
                                 }
  val declare_object : 'a object_declaration -> ('a -> obj)
  val default_object : string -> 'a object_declaration
  val object_tag : obj -> string
end

module Universes :
sig
  type universe_binders = Universes.universe_binders
  type universe_opt_subst = Universes.universe_opt_subst
  val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set
  val new_Type : Names.DirPath.t -> Term.types
  val unsafe_type_of_global : Globnames.global_reference -> Term.types
  val constr_of_global : Prelude.global_reference -> Term.constr
  val new_univ_level : Names.DirPath.t -> Univ.Level.t
  val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context
  val new_sort_in_family : Sorts.family -> Sorts.t
  val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds
  val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
  type universe_constraint = Universes.universe_constraint
  module Constraints :
  sig
    type t = Universes.Constraints.t
    val pr : t -> Pp.std_ppcmds
  end
end

module Global :
sig
  val env : unit -> Environ.env
  val lookup_mind : Names.MutInd.t -> Declarations.mutual_inductive_body
  val lookup_constant  : Names.Constant.t -> Declarations.constant_body
  val lookup_module    : Names.ModPath.t -> Declarations.module_body
  val lookup_modtype   : Names.ModPath.t -> Declarations.module_type_body
  val lookup_inductive : Names.inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body
  val constant_of_delta_kn : Names.KerName.t -> Names.Constant.t
  val register :
    Retroknowledge.field -> Term.constr -> Term.constr -> unit
  val env_of_context : Environ.named_context_val -> Environ.env
  val is_polymorphic : Globnames.global_reference -> bool

  val type_of_global_unsafe : Globnames.global_reference -> Term.types

  val current_dirpath : unit -> Names.DirPath.t
  val body_of_constant_body : Declarations.constant_body -> Term.constr option
  val body_of_constant : Names.Constant.t -> Term.constr option
  val add_constraints : Univ.Constraint.t -> unit
end

module Lib : sig
  type is_type = bool
  type export = bool option
  type node = Lib.node =
            | Leaf of Libobject.obj (* FIX: horrible hack (wrt. Enrico) *)
            | CompilingLibrary of Libnames.object_prefix
            | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen
            | ClosedModule  of library_segment
            | OpenedSection of Libnames.object_prefix * Summary.frozen
            | ClosedSection of library_segment

   and library_segment = (Libnames.object_name * node) list

  val current_mp : unit -> Names.ModPath.t
  val is_modtype : unit -> bool
  val is_module : unit -> bool
  val sections_are_opened : unit -> bool                                        
  val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
  val contents : unit -> library_segment
  val cwd : unit -> Names.DirPath.t
  val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
  val make_kn : Names.Id.t -> Names.KerName.t
  val make_path : Names.Id.t -> Libnames.full_path
  val discharge_con : Names.Constant.t -> Names.Constant.t
  val discharge_inductive : Names.inductive -> Names.inductive
end

module Library :
sig
  val library_is_loaded : Names.DirPath.t -> bool
  val loaded_libraries : unit -> Names.DirPath.t list
end

module Summary :
sig
  type marshallable = Summary.marshallable
  type 'a summary_declaration = 'a Summary.summary_declaration =
    { freeze_function : marshallable -> 'a;
      unfreeze_function : 'a -> unit;
      init_function : unit -> unit; }
  val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
  val declare_summary : string -> 'a summary_declaration -> unit
  module Local :
  sig
    type 'a local_ref = 'a Summary.Local.local_ref
    val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
    val (:=) : 'a local_ref -> 'a -> unit
    val (!) : 'a local_ref -> 'a
  end
end

module Declare :
sig
  type internal_flag = Declare.internal_flag =
    | UserAutomaticRequest
    | InternalTacticRequest
    | UserIndividualRequest
  type constant_declaration = Safe_typing.private_constants Entries.constant_entry * Decl_kinds.logical_kind
  type section_variable_entry = Declare.section_variable_entry =
    | SectionLocalDef of Safe_typing.private_constants Entries.definition_entry
    | SectionLocalAssum of Term.types Univ.in_universe_context_set * Decl_kinds.polymorphic * bool
  type variable_declaration = Names.DirPath.t * section_variable_entry * Decl_kinds.logical_kind
  val declare_constant :
    ?internal:internal_flag -> ?local:bool -> Names.Id.t -> ?export_seff:bool -> constant_declaration -> Names.Constant.t
  val declare_universe_context : Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
  val declare_definition : 
    ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind ->
    ?local:bool -> ?poly:Decl_kinds.polymorphic -> Names.Id.t -> ?types:Term.constr -> 
    Term.constr Univ.in_universe_context_set -> Names.Constant.t
  val definition_entry : ?fix_exn:Future.fix_exn ->
    ?opaque:bool -> ?inline:bool -> ?types:Term.types ->
    ?poly:Decl_kinds.polymorphic -> ?univs:Univ.UContext.t ->
    ?eff:Safe_typing.private_constants -> Term.constr -> Safe_typing.private_constants Entries.definition_entry
  val definition_message : Names.Id.t -> unit
  val declare_variable : Names.Id.t -> variable_declaration -> Libnames.object_name
end

module Reductionops :
sig
  type local_reduction_function = Evd.evar_map -> EConstr.constr -> EConstr.constr

  type reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr

  type local_stack_reduction_function =
    Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list

  type e_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
  type state = Reductionops.state

  val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
  val nf_beta : local_reduction_function
  val nf_betaiota : local_reduction_function
  val splay_prod : Environ.env ->  Evd.evar_map -> EConstr.constr ->
                   (Names.Name.t * EConstr.constr) list * EConstr.constr
  val splay_prod_n : Environ.env ->  Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constr
  val whd_all :  reduction_function
  val whd_beta : local_reduction_function                  

  val whd_betaiotazeta : local_reduction_function

  val whd_betaiota_stack : local_stack_reduction_function

  val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
  val is_conv : ?reds:Names.transparent_state -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
  val beta_applist : Evd.evar_map -> EConstr.constr * EConstr.constr list -> EConstr.constr
  val sort_of_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.ESorts.t
  val is_conv_leq : ?reds:Names.transparent_state -> Environ.env ->  Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
  val whd_betaiota : local_reduction_function
  val is_arity : Environ.env ->  Evd.evar_map -> EConstr.constr -> bool
  val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
  val nf_meta : Evd.evar_map -> EConstr.constr -> EConstr.constr
  val hnf_prod_appvect : Environ.env ->  Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr
  val pr_state : state -> Pp.std_ppcmds
  module Stack :
  sig
    type 'a t = 'a Reductionops.Stack.t
    val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
  end
  module Cst_stack :
  sig
    type t = Reductionops.Cst_stack.t
    val pr : t -> Pp.std_ppcmds
  end
end

module Inductiveops :
sig
  type inductive_family = Inductiveops.inductive_family
  type inductive_type = Inductiveops.inductive_type =
    | IndType of inductive_family * EConstr.constr list
  type constructor_summary = Inductiveops.constructor_summary =
    {
      cs_cstr : Term.pconstructor;
      cs_params : Term.constr list;
      cs_nargs : int;
      cs_args : Context.Rel.t;
      cs_concl_realargs : Term.constr array;
    }

  val arities_of_constructors : Environ.env -> Term.pinductive -> Term.types array
  val constructors_nrealargs_env : Environ.env -> Names.inductive -> int array
  val constructor_nallargs_env : Environ.env -> Names.constructor -> int

  val inductive_nparams : Names.inductive -> int

  val inductive_nparamdecls : Names.inductive -> int

  val type_of_constructors : Environ.env -> Term.pinductive -> Term.types array
  val find_mrectype : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.constr list
  val mis_is_recursive :
    Names.inductive * Declarations.mutual_inductive_body * Declarations.one_inductive_body -> bool
  val nconstructors : Names.inductive -> int
  val find_rectype : Environ.env -> Evd.evar_map -> EConstr.types -> inductive_type
  val get_constructors : Environ.env -> inductive_family -> constructor_summary array
  val dest_ind_family : inductive_family -> Names.inductive Term.puniverses * Term.constr list
  val find_inductive   : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * Term.constr list
  val type_of_inductive : Environ.env -> Term.pinductive -> Term.types
end

module Recordops :
sig
  type cs_pattern = Recordops.cs_pattern =
                  | Const_cs of Globnames.global_reference
                  | Prod_cs
                  | Sort_cs of Sorts.family
                  | Default_cs
  type obj_typ = Recordops.obj_typ = {
        o_DEF : Term.constr;
        o_CTX : Univ.ContextSet.t;
        o_INJ : int option;      (** position of trivial argument *)
        o_TABS : Term.constr list;    (** ordered *)
        o_TPARAMS : Term.constr list; (** ordered *)
        o_NPARAMS : int;
        o_TCOMPS : Term.constr list }
  val lookup_projections : Names.inductive -> Names.Constant.t option list
  val lookup_canonical_conversion : (Globnames.global_reference * cs_pattern) -> Term.constr * obj_typ
  val find_projection_nparams : Globnames.global_reference -> int
end

module Retyping :  (* reconstruct the type of a term knowing that it was already typechecked *)
sig
  val get_type_of : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types
  val get_sort_family_of : ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family
  val expand_projection : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.constr -> EConstr.constr list -> EConstr.constr
  val get_sort_of :
    ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.t
end

module Typing :
sig
  val e_sort_of : Environ.env -> Evd.evar_map ref -> EConstr.types -> Sorts.t

  val type_of : ?refresh:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types
  val e_solve_evars : Environ.env -> Evd.evar_map ref -> EConstr.constr -> EConstr.constr

  val unsafe_type_of : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types

  val e_check : Environ.env -> Evd.evar_map ref -> EConstr.constr -> EConstr.types -> unit

  val e_type_of : ?refresh:bool -> Environ.env -> Evd.evar_map ref -> EConstr.constr -> EConstr.types
end

module Evarsolve :
sig
  val refresh_universes :
    ?status:Evd.rigid -> ?onlyalg:bool -> ?refreshset:bool -> bool option ->
    Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.types
end

module Constr_matching :
sig
  val special_meta : Prelude.metavariable

  type binding_bound_vars = Names.Id.Set.t
  type bound_ident_map = Names.Id.t Names.Id.Map.t
  val is_matching : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> bool
  val extended_matches :
    Environ.env -> Evd.evar_map -> binding_bound_vars * Pattern.constr_pattern ->
    EConstr.constr -> bound_ident_map * Pattern.extended_patvar_map
  exception PatternMatchingFailure
  type matching_result =
    { m_sub : bound_ident_map * Pattern.patvar_map;
      m_ctx : EConstr.constr }
  val match_subterm_gen : Environ.env -> Evd.evar_map ->
                          bool ->
                          binding_bound_vars * Pattern.constr_pattern -> EConstr.constr ->
                          matching_result IStream.t
  val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Pattern.patvar_map
end  

module Tactypes :
sig
  type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
  type glob_constr_pattern_and_expr = Names.Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
  type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
  type delayed_open_constr = EConstr.constr delayed_open
  type delayed_open_constr_with_bindings = EConstr.constr Misctypes.with_bindings delayed_open
  type intro_pattern = delayed_open_constr Misctypes.intro_pattern_expr Loc.located
  type intro_patterns = delayed_open_constr Misctypes.intro_pattern_expr Loc.located list
  type intro_pattern_naming = Misctypes.intro_pattern_naming_expr Loc.located
  type or_and_intro_pattern = delayed_open_constr Misctypes.or_and_intro_pattern_expr Loc.located
end

module Pretyping :
sig
  type typing_constraint = Pretyping.typing_constraint =
                         | OfType of EConstr.types
                         | IsType
                         | WithoutTypeConstraint

  type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> Evd.evar_map * EConstr.constr
  type inference_flags = Pretyping.inference_flags = {
      use_typeclasses : bool;
      solve_unification_constraints : bool;
      use_hook : inference_hook option;
      fail_evar : bool;
      expand_evars : bool
    }

  type pure_open_constr = Evd.evar_map * EConstr.constr
  type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr

  val understand_ltac : inference_flags ->
                        Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map ->
                        typing_constraint -> Glob_term.glob_constr -> pure_open_constr
  val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map ->
                       ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
  val type_uconstr :
    ?flags:inference_flags ->
    ?expected_type:typing_constraint ->
    Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open
  val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
                   Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Term.constr Evd.in_evar_universe_context
  val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
  val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family
  val register_constr_interp0 :
    ('r, 'g, 't) Genarg.genarg_type ->
    (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit
  val all_and_fail_flags : inference_flags
  val ise_pretype_gen :
    inference_flags -> Environ.env -> Evd.evar_map ->
    Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
end

module Evarconv :
sig
  val e_conv : Environ.env -> ?ts:Names.transparent_state -> Evd.evar_map ref -> EConstr.constr -> EConstr.constr -> bool
  val the_conv_x : Environ.env -> ?ts:Names.transparent_state -> EConstr.constr -> EConstr.constr -> Evd.evar_map -> Evd.evar_map
  val the_conv_x_leq : Environ.env -> ?ts:Names.transparent_state -> EConstr.constr -> EConstr.constr -> Evd.evar_map -> Evd.evar_map
  val solve_unif_constraints_with_heuristics : Environ.env -> ?ts:Names.transparent_state -> Evd.evar_map -> Evd.evar_map
end

module Unification :
sig
  type core_unify_flags = Unification.core_unify_flags =
                            {
                              modulo_conv_on_closed_terms : Names.transparent_state option;
                              use_metas_eagerly_in_conv_on_closed_terms : bool;
                              use_evars_eagerly_in_conv_on_closed_terms : bool;
                              modulo_delta : Names.transparent_state;
                              modulo_delta_types : Names.transparent_state;
                              check_applied_meta_types : bool;
                              use_pattern_unification : bool;
                              use_meta_bound_pattern_unification : bool;
                              frozen_evars : Evar.Set.t;
                              restrict_conv_on_strict_subterms : bool;
                              modulo_betaiota : bool;
                              modulo_eta : bool;
                            }
  type unify_flags = Unification.unify_flags =
                       {
                         core_unify_flags : core_unify_flags;
                         merge_unify_flags : core_unify_flags;
                         subterm_unify_flags : core_unify_flags;
                         allow_K_in_toplevel_higher_order_unification : bool;
                         resolve_evars : bool
                       }
  val default_no_delta_unify_flags : unit -> unify_flags
  val w_unify : Environ.env -> Evd.evar_map -> Reduction.conv_pb -> ?flags:unify_flags -> EConstr.constr -> EConstr.constr -> Evd.evar_map
  val elim_flags : unit -> unify_flags
  val w_unify_to_subterm :
    Environ.env -> Evd.evar_map -> ?flags:unify_flags -> EConstr.constr * EConstr.constr -> Evd.evar_map * EConstr.constr
end

module Typeclasses :
sig
  type typeclass = Typeclasses.typeclass = {
    cl_impl : Globnames.global_reference;
    cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t;
    cl_props : Context.Rel.t;
    cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option
                * Names.Constant.t option) list;
    cl_strict : bool;
    cl_unique : bool;
  }
   and direction = Typeclasses.direction
  type instance = Typeclasses.instance
  type evar_filter = Evar.t -> Evar_kinds.t -> bool
  val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
                            ?split:bool -> ?fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map
  val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t
  val resolve_one_typeclass : ?unique:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.constr
  val class_info : Globnames.global_reference -> typeclass
  val mark_resolvables : ?filter:evar_filter -> Evd.evar_map -> Evd.evar_map
  val add_instance : instance -> unit
  val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
                     Globnames.global_reference -> instance
end

module Pretype_errors :
sig
  type unification_error = Pretype_errors.unification_error
  type subterm_unification_error = Pretype_errors.subterm_unification_error
  type pretype_error = Pretype_errors.pretype_error =
                     | CantFindCaseType of EConstr.constr
                     | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
                     | UnifOccurCheck of Evar.t * EConstr.constr
                     | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option
                     | CannotUnify of EConstr.constr * EConstr.constr * unification_error option
                     | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr
                     | CannotUnifyBindingType of EConstr.constr * EConstr.constr
                     | CannotGeneralize of EConstr.constr
                     | NoOccurrenceFound of EConstr.constr * Names.Id.t option
                     | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (Environ.env * Pretype_errors.type_error) option
                     | WrongAbstractionType of Names.Name.t * EConstr.constr * EConstr.types * EConstr.types
                     | AbstractionOverMeta of Names.Name.t * Names.Name.t
                     | NonLinearUnification of Names.Name.t * EConstr.constr
                     | VarNotFound of Names.Id.t
                     | UnexpectedType of EConstr.constr * EConstr.constr
                     | NotProduct of EConstr.constr
                     | TypingError of Pretype_errors.type_error
                     | CannotUnifyOccurrences of subterm_unification_error
                     | UnsatisfiableConstraints of
                         (Evar.t * Evar_kinds.t) option * Evar.Set.t option

  exception PretypeError of Environ.env * Evd.evar_map * pretype_error
  val error_var_not_found : ?loc:Loc.t -> Names.Id.t -> 'b
  val precatchable_exception : exn -> bool
end

module Smartlocate :
sig
  val locate_global_with_alias : ?head:bool -> Libnames.qualid Loc.located -> Globnames.global_reference
  val global_with_alias : ?head:bool -> Prelude.reference -> Globnames.global_reference
  val global_of_extended_global : Globnames.extended_global_reference -> Globnames.global_reference
  val loc_of_smart_reference : Prelude.reference Misctypes.or_by_notation -> Loc.t option
  val smart_global : ?head:bool -> Prelude.reference Misctypes.or_by_notation -> Globnames.global_reference
end

module Dumpglob :
sig
  val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
  val pause : unit -> unit
  val continue : unit -> unit
end

module Stdarg :
sig
  val loc_of_or_by_notation : ('a -> Loc.t option) -> 'a Misctypes.or_by_notation -> Loc.t option
  val wit_unit : unit Genarg.uniform_genarg_type
  val wit_int : int Genarg.uniform_genarg_type
  val wit_var : (Names.Id.t Loc.located, Names.Id.t Loc.located, Names.Id.t) Genarg.genarg_type
  val wit_bool : bool Genarg.uniform_genarg_type
  val wit_string : string Genarg.uniform_genarg_type
  val wit_pre_ident : string Genarg.uniform_genarg_type
  val wit_global : (Prelude.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type
  val wit_ident : Names.Id.t Genarg.uniform_genarg_type
  val wit_integer : int Genarg.uniform_genarg_type
  val wit_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type
  val wit_open_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type
  val wit_intro_pattern : (Constrexpr.constr_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.glob_constr_and_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.intro_pattern) Genarg.genarg_type
  val wit_int_or_var : (int Misctypes.or_var, int Misctypes.or_var, int) Genarg.genarg_type
  val wit_ref : (Prelude.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type
  val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) Genarg.genarg_type
  val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Glob_term.closed_glob_constr) Genarg.genarg_type
  val wit_red_expr :
    ((Constrexpr.constr_expr,Prelude.reference Misctypes.or_by_notation,Constrexpr.constr_expr) Genredexpr.red_expr_gen,
     (Tactypes.glob_constr_and_expr,Names.evaluable_global_reference Misctypes.and_short_name Misctypes.or_var,Tactypes.glob_constr_pattern_and_expr) Genredexpr.red_expr_gen,
     (EConstr.constr,Names.evaluable_global_reference,Pattern.constr_pattern) Genredexpr.red_expr_gen) Genarg.genarg_type
  val wit_quant_hyp : Misctypes.quantified_hypothesis Genarg.uniform_genarg_type
  val wit_bindings :
    (Constrexpr.constr_expr Misctypes.bindings,
     Tactypes.glob_constr_and_expr Misctypes.bindings,
     EConstr.constr Misctypes.bindings Tactypes.delayed_open) Genarg.genarg_type
  val wit_constr_with_bindings :
    (Constrexpr.constr_expr Misctypes.with_bindings,
     Tactypes.glob_constr_and_expr Misctypes.with_bindings,
     EConstr.constr Misctypes.with_bindings Tactypes.delayed_open) Genarg.genarg_type
  val wit_intropattern : (Constrexpr.constr_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.glob_constr_and_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.intro_pattern) Genarg.genarg_type
  val wit_quantified_hypothesis : Misctypes.quantified_hypothesis Genarg.uniform_genarg_type
  val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) Genarg.genarg_type
  val wit_preident : string Genarg.uniform_genarg_type
  val wit_reference : (Prelude.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type
  val wit_open_constr_with_bindings :
    (Constrexpr.constr_expr Misctypes.with_bindings,
     Tactypes.glob_constr_and_expr Misctypes.with_bindings,
     EConstr.constr Misctypes.with_bindings Tactypes.delayed_open) Genarg.genarg_type
end

module Coqlib :
sig
  type coq_eq_data = Coqlib.coq_eq_data = { eq   : Globnames.global_reference;
                                            ind  : Globnames.global_reference;
                                            refl : Globnames.global_reference;
                                            sym  : Globnames.global_reference;
                                            trans: Globnames.global_reference;
                                            congr: Globnames.global_reference;
                                          }
  type coq_sigma_data = Coqlib.coq_sigma_data = {
      proj1 : Globnames.global_reference;
      proj2 : Globnames.global_reference;
      elim  : Globnames.global_reference;
      intro : Globnames.global_reference;
      typ   : Globnames.global_reference }
  val gen_reference : string -> string list -> string -> Globnames.global_reference
  val find_reference : string -> string list -> string -> Globnames.global_reference
  val check_required_library : string list -> unit
  val logic_module_name : string list
  val glob_true : Globnames.global_reference
  val glob_false : Globnames.global_reference
  val glob_O : Globnames.global_reference
  val glob_S : Globnames.global_reference
  val nat_path : Libnames.full_path
  val datatypes_module_name : string list
  val glob_eq : Globnames.global_reference
  val build_coq_eq_sym : Globnames.global_reference Util.delayed
  val build_coq_False : Globnames.global_reference Util.delayed
  val build_coq_not : Globnames.global_reference Util.delayed
  val build_coq_eq : Globnames.global_reference Util.delayed
  val build_coq_eq_data : coq_eq_data Util.delayed
  val path_of_O : Names.constructor
  val path_of_S : Names.constructor
  val build_prod : coq_sigma_data Util.delayed
  val build_coq_True : Globnames.global_reference Util.delayed
  val coq_iff_ref : Globnames.global_reference lazy_t
  val build_coq_iff_left_proj : Globnames.global_reference Util.delayed
  val build_coq_iff_right_proj : Globnames.global_reference Util.delayed
  val init_modules : string list list
  val build_coq_eq_refl  : Globnames.global_reference Util.delayed
  val arith_modules : string list list
  val zarith_base_modules : string list list
  val gen_reference_in_modules : string -> string list list-> string -> Globnames.global_reference
  val jmeq_module_name : string list
  val coq_eq_ref : Globnames.global_reference lazy_t
  val coq_not_ref : Globnames.global_reference lazy_t
  val coq_or_ref : Globnames.global_reference lazy_t
  val build_coq_and : Globnames.global_reference Util.delayed
  val build_coq_I : Globnames.global_reference Util.delayed
  val coq_reference : string -> string list -> string -> Globnames.global_reference
end

module Impargs :
sig
  type implicit_status = Impargs.implicit_status
  type implicit_side_condition = Impargs.implicit_side_condition
  type implicits_list = implicit_side_condition * implicit_status list
  type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
  type manual_implicits = manual_explicitation list
  val is_status_implicit : implicit_status -> bool
  val name_of_implicit : implicit_status -> Names.Id.t
  val implicits_of_global : Globnames.global_reference -> implicits_list list
  val declare_manual_implicits : bool -> Globnames.global_reference -> ?enriching:bool ->
                                 manual_implicits list -> unit
  val is_implicit_args : unit -> bool
  val is_strict_implicit_args : unit -> bool
  val is_contextual_implicit_args : unit -> bool
  val make_implicit_args : bool -> unit
  val make_strict_implicit_args : bool -> unit
  val make_contextual_implicit_args : bool -> unit
end

module Constrintern :
sig
  type ltac_sign = Constrintern.ltac_sign = {
        ltac_vars : Names.Id.Set.t;
        ltac_bound : Names.Id.Set.t;
        ltac_extra : Genintern.Store.t;
      }
  type var_internalization_data = Constrintern.var_internalization_data
  type var_internalization_type = Constrintern.var_internalization_type =
    | Inductive of Names.Id.t list * bool
    | Recursive
    | Method
    | Variable
  type internalization_env = var_internalization_data Names.Id.Map.t

  val interp_constr_evars : Environ.env -> Evd.evar_map ref ->
                            ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.constr

  val interp_type_evars : Environ.env -> Evd.evar_map ref ->
                          ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types

  val empty_ltac_sign : ltac_sign
  val intern_gen : Pretyping.typing_constraint -> Environ.env ->
                   ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
                   Constrexpr.constr_expr -> Glob_term.glob_constr
  val intern_constr_pattern :
    Environ.env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
    Constrexpr.constr_pattern_expr -> Names.Id.t list * Pattern.constr_pattern
  val intern_constr : Environ.env -> Constrexpr.constr_expr -> Glob_term.glob_constr
  val for_grammar : ('a -> 'b) -> 'a -> 'b
  val interp_reference : ltac_sign -> Prelude.reference -> Glob_term.glob_constr
  val interp_constr : Environ.env -> Evd.evar_map -> ?impls:internalization_env ->
                      Constrexpr.constr_expr -> Term.constr Evd.in_evar_universe_context
  val interp_open_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.constr
  val locate_reference :  Libnames.qualid -> Globnames.global_reference
  val interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env ->
                    Constrexpr.constr_expr -> Term.types Evd.in_evar_universe_context
  val interp_context_evars :
    ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
    Environ.env -> Evd.evar_map ref -> Constrexpr.local_binder_expr list ->
    internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits)
  val compute_internalization_data : Environ.env -> var_internalization_type ->
                                     Term.types -> Impargs.manual_explicitation list -> var_internalization_data
  val empty_internalization_env : internalization_env
  val global_reference : Names.Id.t -> Globnames.global_reference
end

module Notation_term :
sig
  type scope_name = string
  type notation_var_instance_type = Notation_term.notation_var_instance_type =
                                  | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList
  type tmp_scope_name = Notation_term.tmp_scope_name
  type subscopes = tmp_scope_name option * scope_name list
  type notation_constr = Notation_term.notation_constr =
                       | NRef of Globnames.global_reference
                       | NVar of Names.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 Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool
                       | NLambda of Names.Name.t * notation_constr * notation_constr
                       | NProd of Names.Name.t * notation_constr * notation_constr
                       | NBinderList of Names.Id.t * Names.Id.t * notation_constr * notation_constr
                       | NLetIn of Names.Name.t * notation_constr * notation_constr option * notation_constr
                       | NCases of Term.case_style * notation_constr option *
                                     (notation_constr * (Names.Name.t * (Names.inductive * Names.Name.t list) option)) list *
                                       (Glob_term.cases_pattern list * notation_constr) list
                       | NLetTuple of Names.Name.t list * (Names.Name.t * notation_constr option) *
                                        notation_constr * notation_constr
                       | NIf of notation_constr * (Names.Name.t * notation_constr option) *
                                  notation_constr * notation_constr
                       | NRec of Glob_term.fix_kind * Names.Id.t array *
                                   (Names.Name.t * notation_constr option * notation_constr) list array *
                                     notation_constr array * notation_constr array
                       | NSort of Misctypes.glob_sort
                       | NCast of notation_constr * notation_constr Misctypes.cast_type
  type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list *
    notation_constr
end

module Notation :
sig
  type cases_pattern_status = bool
  type required_module = Libnames.full_path * string list
  type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> Glob_term.glob_constr
  type 'a prim_token_uninterpreter = Glob_term.glob_constr list * (Glob_term.glob_constr -> 'a option) * cases_pattern_status
  type delimiters = string
  type local_scopes = Notation_term.tmp_scope_name option * Notation_term.scope_name list
  type notation_location = (Names.DirPath.t * Names.DirPath.t) * string
  val declare_string_interpreter : Notation_term.scope_name -> required_module ->
                                   string prim_token_interpreter -> string prim_token_uninterpreter -> unit
  val declare_numeral_interpreter : Notation_term.scope_name -> required_module ->
                                    Bigint.bigint prim_token_interpreter -> Bigint.bigint prim_token_uninterpreter -> unit
  val interp_notation_as_global_reference : ?loc:Loc.t -> (Globnames.global_reference -> bool) ->
                                            Constrexpr.notation -> delimiters option -> Globnames.global_reference
  val locate_notation : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Constrexpr.notation ->
                        Notation_term.scope_name option -> Pp.std_ppcmds
  val find_delimiters_scope : ?loc:Loc.t -> delimiters -> Notation_term.scope_name
  val pr_scope : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Notation_term.scope_name -> Pp.std_ppcmds
  val pr_scopes : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Pp.std_ppcmds
  val interp_notation : ?loc:Loc.t -> Constrexpr.notation -> local_scopes ->
                        Notation_term.interpretation * (notation_location * Notation_term.scope_name option)
  val uninterp_prim_token : Glob_term.glob_constr -> Notation_term.scope_name * Constrexpr.prim_token
end

module Mltop :
sig
  val declare_cache_obj : (unit -> unit) -> string -> unit
  val add_known_plugin : (unit -> unit) -> string -> unit
  val add_known_module : string -> unit
  val module_is_known : string -> bool
end

(* All items in the Proof_type module are deprecated. *)
module Proof_type :
sig
  type goal = Evar.t
  type rule = Proof_type.prim_rule =
    | Cut of bool * bool * Names.Id.t * Term.types
    | Refine of Term.constr

  type tactic = goal Evd.sigma -> goal list Evd.sigma
end

module Redexpr :
sig
  type red_expr =
    (EConstr.constr, Names.evaluable_global_reference, Pattern.constr_pattern) Genredexpr.red_expr_gen
  val reduction_of_red_expr :
    Environ.env -> red_expr -> Reductionops.e_reduction_function * Term.cast_kind
  val declare_reduction : string -> Reductionops.reduction_function -> unit
end

module Tacmach :
sig
  type tactic = Proof_type.tactic
  [@@ocaml.deprecated "alias for API.Proof_type.tactic"]

  type 'a sigma = 'a Evd.sigma
  [@@ocaml.deprecated "alias of API.Evd.sigma"]

  val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma

  val pf_reduction_of_red_expr : Proof_type.goal Evd.sigma -> Redexpr.red_expr -> EConstr.constr -> Evd.evar_map * EConstr.constr

  val pf_unsafe_type_of : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.types

  val pf_get_new_id  : Names.Id.t -> Proof_type.goal Evd.sigma -> Names.Id.t

  val pf_env : Proof_type.goal Evd.sigma -> Environ.env

  val pf_concl : Proof_type.goal Evd.sigma -> EConstr.types

  val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Proof_type.goal Evd.sigma -> 'a

  val pf_get_hyp            : Proof_type.goal Evd.sigma -> Names.Id.t -> EConstr.named_declaration
  val pf_get_hyp_typ        : Proof_type.goal Evd.sigma -> Names.Id.t -> EConstr.types
  val project : Proof_type.goal Evd.sigma -> Evd.evar_map
  val refine : EConstr.constr -> Proof_type.tactic
  val pf_type_of : Proof_type.goal Evd.sigma -> EConstr.constr -> Evd.evar_map * EConstr.types

  val pf_hyps : Proof_type.goal Evd.sigma -> EConstr.named_context

  val pf_ids_of_hyps : Proof_type.goal Evd.sigma -> Names.Id.t list

  val pf_reduce_to_atomic_ind : Proof_type.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types

  val pf_reduce_to_quantified_ind : Proof_type.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types

  val pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) -> 
                  Evar.t Evd.sigma -> 'a -> Evar.t Evd.sigma * 'b

  val pf_unfoldn : (Locus.occurrences * Names.evaluable_global_reference) list
                   -> Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr

  val pf_reduce : (Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr) -> Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr

  val pf_conv_x : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool

  val pf_is_matching : Proof_type.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool

  val pf_hyps_types : Proof_type.goal Evd.sigma -> (Names.Id.t * EConstr.types) list

  val pr_gls    : Proof_type.goal Evd.sigma -> Pp.std_ppcmds

  val pf_nf_betaiota : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr

  val pf_last_hyp : Proof_type.goal Evd.sigma -> EConstr.named_declaration

  val pf_nth_hyp_id : Proof_type.goal Evd.sigma -> int -> Names.Id.t

  val sig_it : 'a Evd.sigma -> 'a

  module New :
  sig
    val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
    val project : 'a Proofview.Goal.t -> Evd.evar_map
    val pf_unsafe_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
    val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a

    val pf_env : 'a Proofview.Goal.t -> Environ.env
    val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list
    val pf_concl : 'a Proofview.Goal.t -> EConstr.types
    val pf_get_new_id  : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t
    val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types
    val pf_get_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
    val pf_global : Names.Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference
    val pf_hyps_types : 'a Proofview.Goal.t -> (Names.Id.t * EConstr.types) list
  end
end

module Proof :
sig
  type proof = Proof.proof
  type 'a focus_kind = 'a Proof.focus_kind
  val run_tactic : Environ.env ->
                   unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree)
  val unshelve : proof -> proof
  val maximal_unfocus : 'a focus_kind -> proof -> proof
  val pr_proof : proof -> Pp.std_ppcmds
  module V82 :
  sig
    val grab_evars : proof -> proof

    val subgoals : proof -> Goal.goal list Evd.sigma
  end
end

module Proof_global :
sig
  type proof_mode = Proof_global.proof_mode = {
      name : string;
      set : unit -> unit ;
      reset : unit -> unit
    }
  type proof_universes = UState.t * Universes.universe_binders option
  type proof_object = Proof_global.proof_object = {
        id : Names.Id.t;
        entries : Safe_typing.private_constants Entries.definition_entry list;
        persistence : Decl_kinds.goal_kind;
        universes: proof_universes;
      }
  type proof_ending = Proof_global.proof_ending =
  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
                  proof_universes
  | Proved of Vernacexpr.opacity_flag *
              Vernacexpr.lident option *
              proof_object
  type proof_terminator = Proof_global.proof_terminator
  type lemma_possible_guards = Proof_global.lemma_possible_guards
  type universe_binders = Proof_global.universe_binders
  type closed_proof = proof_object * proof_terminator
  val make_terminator : (proof_ending -> unit) -> proof_terminator
  val start_dependent_proof :
    Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind ->
    Proofview.telescope -> proof_terminator -> unit
  val with_current_proof :
    (unit Proofview.tactic -> Proof.proof -> Proof.proof * 'a) -> 'a
  val simple_with_current_proof :
    (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
  val compact_the_proof : unit -> unit
  val register_proof_mode : proof_mode -> unit
  val get_default_goal_selector : unit -> Vernacexpr.goal_selector

  exception NoCurrentProof
  val give_me_the_proof : unit -> Proof.proof
  (** @raise NoCurrentProof when outside proof mode. *)

  val discard_all : unit -> unit
  val discard_current : unit -> unit
  val get_current_proof_name : unit -> Names.Id.t
end

module Nametab :
sig
  exception GlobalizationError of Libnames.qualid

  type ltac_constant = Names.KerName.t

  val global_of_path : Libnames.full_path -> Globnames.global_reference
  val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid
  val path_of_global : Globnames.global_reference -> Libnames.full_path
  val locate_extended : Libnames.qualid -> Globnames.extended_global_reference
  val full_name_module : Libnames.qualid -> Names.DirPath.t
  val locate_tactic : Libnames.qualid -> Names.KerName.t
  val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.std_ppcmds
  val shortest_qualid_of_tactic : Names.KerName.t -> Libnames.qualid
  val basename_of_global : Globnames.global_reference -> Names.Id.t

  type visibility = Nametab.visibility =
                  | Until of int
                  | Exactly of int

  val push_tactic : visibility -> Libnames.full_path -> Names.KerName.t -> unit
  val error_global_not_found : ?loc:Loc.t -> Libnames.qualid -> 'a
  val shortest_qualid_of_module : Names.ModPath.t -> Libnames.qualid
  val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t
  val locate_module : Libnames.qualid -> Names.ModPath.t
  val dirpath_of_global : Globnames.global_reference -> Names.DirPath.t
  val locate : Libnames.qualid -> Globnames.global_reference
  val locate_constant : Libnames.qualid -> Names.Constant.t
end

module Ppextend :
sig
  type precedence = int
  type parenRelation = Ppextend.parenRelation =
                     | L | E | Any | Prec of precedence
  type tolerability = precedence * parenRelation
end

module Refiner :
sig
  val project : 'a Evd.sigma -> Evd.evar_map
  
  val unpackage : 'a Evd.sigma -> Evd.evar_map ref * 'a

  val repackage : Evd.evar_map ref -> 'a -> 'a Evd.sigma

  val refiner : Proof_type.rule -> Proof_type.tactic

  val tclSHOWHYPS : Proof_type.tactic -> Proof_type.tactic
  exception FailError of int * Pp.std_ppcmds Lazy.t

  val tclEVARS : Evd.evar_map -> Proof_type.tactic
  val tclMAP : ('a -> Proof_type.tactic) -> 'a list -> Proof_type.tactic
  val tclREPEAT : Proof_type.tactic -> Proof_type.tactic
  val tclORELSE        : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
  val tclFAIL : int -> Pp.std_ppcmds -> Proof_type.tactic
  val tclIDTAC : Proof_type.tactic
  val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
  val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic
  val tclTRY : Proof_type.tactic -> Proof_type.tactic
  val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic
end

module Termops :
sig
  val it_mkLambda_or_LetIn : Term.constr -> Context.Rel.t -> Term.constr
  val local_occur_var : Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
  val occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
  val pr_evar_info : Evd.evar_info -> Pp.std_ppcmds

  val print_constr : EConstr.constr -> Pp.std_ppcmds

  (** [dependent m t] tests whether [m] is a subterm of [t] *)
  val dependent : Prelude.evar_map -> EConstr.constr -> EConstr.constr -> bool

  (** [pop c] returns a copy of [c] with decremented De Bruijn indexes *)
  val pop : EConstr.constr -> EConstr.constr

  (** Does a given term contain an existential variable? *)
  val occur_existential : Prelude.evar_map -> EConstr.constr -> bool

  (** [map_constr_with_binders_left_to_right g f acc c] maps [f updated_acc] on all the immediate subterms of [c].
      {ul {- if a given immediate subterm of [c] is not below a binder, then [updated_acc] is the same as [acc].}
          {- if a given immediate subterm of [c] is below a binder [b], then [updated_acc] is computed as [g b acc].}} *)
  val map_constr_with_binders_left_to_right :
    Prelude.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr

  (** Remove the outer-most {!Term.kind_of_term.Cast} from a given term. *)
  val strip_outer_cast : Prelude.evar_map -> EConstr.constr -> EConstr.constr

  (** [nb_lam] ⟦[fun (x1:t1)...(xn:tn) => c]⟧ where [c] is not an abstraction gives [n].
      Casts are ignored. *)
  val nb_lam : Prelude.evar_map -> EConstr.constr -> int

  (** [push_rel_assum env_assumtion env] adds a given {i env assumption} to the {i env context} of a given {i environment}. *)
  val push_rel_assum : Names.Name.t * EConstr.types -> Environ.env -> Environ.env

  (** [push_rels_assum env_assumptions env] adds given {i env assumptions} to the {i env context} of a given {i environment}. *)
  val push_rels_assum : (Names.Name.t * Term.types) list -> Environ.env -> Environ.env

  type meta_value_map = Prelude.meta_value_map

  val last_arg : Evd.evar_map -> EConstr.constr -> EConstr.constr
  val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Names.Name.t * 't) list
  val prod_applist : Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr
  val nb_prod : Evd.evar_map -> EConstr.constr -> int
  val is_section_variable : Names.Id.t -> bool
  val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Names.Id.t list
  val subst_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constr
  val global_vars_set_of_decl : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Names.Id.Set.t
  val vars_of_env: Environ.env -> Names.Id.Set.t
  val ids_of_named_context : ('c, 't) Context.Named.pt -> Names.Id.t list
  val ids_of_context : Environ.env -> Names.Id.t list
  val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference * EConstr.EInstance.t
  val print_named_context : Environ.env -> Pp.std_ppcmds
  val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds
  val clear_named_body : Names.Id.t -> Environ.env -> Environ.env
  val is_Prop : Evd.evar_map -> EConstr.constr -> bool
  val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool

  val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool

  val occur_var_in_decl :
    Environ.env -> Evd.evar_map ->
    Names.Id.t -> EConstr.named_declaration -> bool

  val subst_meta : Prelude.meta_value_map -> Term.constr -> Term.constr

  val free_rels : Evd.evar_map -> EConstr.constr -> Int.Set.t

  val occur_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
  [@@ocaml.deprecated "alias of API.Termops.dependent"]

  val replace_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
  val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
  val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
  val pr_metaset : Evd.Metaset.t -> Pp.std_ppcmds
  val pr_evar_map : ?with_univs:bool -> int option -> Evd.evar_map -> Pp.std_ppcmds
  val pr_evar_universe_context : UState.t -> Pp.std_ppcmds
end

module Locality :
sig
  val make_section_locality : bool option -> bool
  module LocalityFixme : sig
    val consume : unit -> bool option
  end
  val make_module_locality : bool option -> bool
end

module Search :
sig
  type glob_search_about_item = Search.glob_search_about_item =
                              | GlobSearchSubPattern of Pattern.constr_pattern
                              | GlobSearchString of string
  type filter_function = Globnames.global_reference -> Environ.env -> Term.constr -> bool
  type display_function = Globnames.global_reference -> Environ.env -> Term.constr -> unit
  val search_about_filter : glob_search_about_item -> filter_function
  val module_filter : Names.DirPath.t list * bool -> filter_function
  val generic_search : int option -> display_function -> unit
end

module Notation_ops :
sig
  val glob_constr_of_notation_constr : ?loc:Loc.t -> Notation_term.notation_constr -> Glob_term.glob_constr
  val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
                                                    ('a -> Names.Name.t -> 'a * Names.Name.t) ->
                                                    ('a -> Notation_term.notation_constr -> Glob_term.glob_constr) ->
                                                    'a -> Notation_term.notation_constr -> Glob_term.glob_constr
end

module Constrextern :
sig
  val extern_glob_constr : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr
  val extern_glob_type : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr
  val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> Term.constr -> Constrexpr.constr_expr
  val without_symbols : ('a -> 'b) -> 'a -> 'b
  val print_universes : bool ref
  val extern_type : bool -> Environ.env -> Evd.evar_map -> Term.types -> Constrexpr.constr_expr
  val with_universes : ('a -> 'b) -> 'a -> 'b
  val set_extern_reference :
    (?loc:Loc.t -> Names.Id.Set.t -> Globnames.global_reference -> Libnames.reference) -> unit
end

module Patternops :
sig
  val pattern_of_glob_constr : Glob_term.glob_constr -> Names.Id.t list * Pattern.constr_pattern
  val subst_pattern : Mod_subst.substitution -> Pattern.constr_pattern -> Pattern.constr_pattern
  val pattern_of_constr : Environ.env -> Evd.evar_map -> Term.constr -> Pattern.constr_pattern
  val instantiate_pattern : Environ.env ->
    Evd.evar_map -> Pattern.extended_patvar_map ->
    Pattern.constr_pattern -> Pattern.constr_pattern
end

module Printer :
sig
  val pr_named_context : Environ.env -> Evd.evar_map -> Context.Named.t -> Pp.std_ppcmds
  val pr_rel_context : Environ.env -> Evd.evar_map -> Context.Rel.t -> Pp.std_ppcmds
  val pr_goal : Proof_type.goal Evd.sigma -> Pp.std_ppcmds

  val pr_constr_env : Prelude.env -> Prelude.evar_map -> Term.constr -> Pp.std_ppcmds
  val pr_lconstr_env : Prelude.env -> Prelude.evar_map -> Term.constr -> Pp.std_ppcmds

  val pr_constr : Term.constr -> Pp.std_ppcmds

  val pr_lconstr : Term.constr -> Pp.std_ppcmds

  val pr_econstr : EConstr.constr -> Pp.std_ppcmds
  val pr_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds
  val pr_constr_pattern : Pattern.constr_pattern -> Pp.std_ppcmds
  val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.std_ppcmds
  val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.std_ppcmds
  val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds
  val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.std_ppcmds
  val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.std_ppcmds
  val pr_closed_glob : Glob_term.closed_glob_constr -> Pp.std_ppcmds
  val pr_lglob_constr : Glob_term.glob_constr -> Pp.std_ppcmds
  val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds
  val pr_leconstr : EConstr.constr -> Pp.std_ppcmds
  val pr_global : Globnames.global_reference -> Pp.std_ppcmds
  val pr_lconstr_under_binders : Pattern.constr_under_binders -> Pp.std_ppcmds
  val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.std_ppcmds

  val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.std_ppcmds
  val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Pp.std_ppcmds
  val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds
  val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds
  val pr_ltype : Term.types -> Pp.std_ppcmds
  val pr_ljudge : EConstr.unsafe_judgment -> Pp.std_ppcmds * Pp.std_ppcmds
  val pr_idpred : Names.Id.Pred.t -> Pp.std_ppcmds
  val pr_cpred : Names.Cpred.t -> Pp.std_ppcmds
  val pr_transparent_state : Names.transparent_state -> Pp.std_ppcmds
end

module Classes :
sig
  val set_typeclass_transparency : Names.evaluable_global_reference -> bool -> bool -> unit
  val new_instance :
    ?abstract:bool ->
    ?global:bool ->
    ?refine:bool ->
    Decl_kinds.polymorphic ->
    Constrexpr.local_binder_expr list ->
    Constrexpr.typeclass_constraint ->
    (bool * Constrexpr.constr_expr) option ->
    ?generalize:bool ->
    ?tac:unit Proofview.tactic  ->
    ?hook:(Globnames.global_reference -> unit) ->
    Vernacexpr.hint_info_expr ->
    Names.Id.t
end

module Classops :
sig
  type coe_index = Classops.coe_index
  type inheritance_path = coe_index list
  type cl_index = Classops.cl_index

  val hide_coercion : Globnames.global_reference -> int option
  val lookup_path_to_sort_from : Environ.env -> Evd.evar_map -> EConstr.types ->
                                 EConstr.types * inheritance_path
  val get_coercion_value : coe_index -> Constr.t
  val coercions : unit -> coe_index list
  val pr_cl_index : cl_index -> Pp.std_ppcmds
end

module ExplainErr :
sig
  val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
  val register_additional_error_info : (Util.iexn -> Pp.std_ppcmds option Loc.located option) -> unit
end

module Tacred :
sig
  val try_red_product : Reductionops.reduction_function
  val simpl : Reductionops.reduction_function
  val unfoldn :
    (Locus.occurrences * Names.evaluable_global_reference) list ->  Reductionops.reduction_function
  val hnf_constr : Reductionops.reduction_function
  val red_product : Reductionops.reduction_function
  val is_evaluable : Environ.env -> Names.evaluable_global_reference -> bool
  val evaluable_of_global_reference :
    Environ.env -> Globnames.global_reference -> Names.evaluable_global_reference
  val error_not_evaluable : Globnames.global_reference -> 'a
  val reduce_to_quantified_ref :
    Environ.env ->  Evd.evar_map -> Globnames.global_reference -> EConstr.types -> EConstr.types
  val pattern_occs : (Locus.occurrences * EConstr.constr) list -> Reductionops.e_reduction_function
  val cbv_norm_flags : CClosure.RedFlags.reds -> Reductionops.reduction_function
end

module Detyping :
sig
  val print_universes : bool ref
  val print_evar_arguments : bool ref
  val detype : ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> Glob_term.glob_constr
  val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr
  val set_detype_anonymous : (?loc:Loc.t -> int -> Glob_term.glob_constr) -> unit
end

module Constrexpr_ops :
sig
  val mkIdentC : Names.Id.t -> Constrexpr.constr_expr
  val mkAppC : Constrexpr.constr_expr * Constrexpr.constr_expr list -> Constrexpr.constr_expr
  val names_of_local_assums : Constrexpr.local_binder_expr list -> Names.Name.t Loc.located list
  val coerce_reference_to_id : Prelude.reference -> Names.Id.t
  val coerce_to_id : Constrexpr.constr_expr -> Names.Id.t Loc.located
  val constr_loc : Constrexpr.constr_expr -> Loc.t option
  val mkRefC : Prelude.reference -> Constrexpr.constr_expr
  val mkLambdaC : Names.Name.t Loc.located list * Constrexpr.binder_kind * Constrexpr.constr_expr * Constrexpr.constr_expr -> Constrexpr.constr_expr
  val default_binder_kind : Constrexpr.binder_kind
  val mkLetInC : Names.Name.t Loc.located * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr -> Constrexpr.constr_expr
  val mkCProdN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr
end

module Glob_ops :
sig
  val map_glob_constr_left_to_right : (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr
  val loc_of_glob_constr : Glob_term.glob_constr -> Loc.t option
  val glob_constr_eq : Glob_term.glob_constr -> Glob_term.glob_constr -> bool
  val bound_glob_vars : Glob_term.glob_constr -> Names.Id.Set.t

  (** Conversion from glob_constr to cases pattern, if possible

    Take the current alias as parameter,
    @raise Not_found if translation is impossible *)
  val cases_pattern_of_glob_constr : Names.Name.t -> Glob_term.glob_constr -> Glob_term.cases_pattern
  val map_glob_constr :
    (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr
  val empty_lvar : Glob_term.ltac_var_map
end

module Indrec :
sig
  type dep_flag = bool
  val lookup_eliminator : Names.inductive -> Sorts.family -> Globnames.global_reference
  val build_case_analysis_scheme : Environ.env -> Evd.evar_map -> Term.pinductive ->
                                   dep_flag -> Sorts.family -> Evd.evar_map * Term.constr
  val make_elimination_ident : Names.Id.t -> Sorts.family -> Names.Id.t
  val build_mutual_induction_scheme :
    Environ.env -> Evd.evar_map -> (Term.pinductive * dep_flag * Sorts.family) list -> Evd.evar_map * Term.constr list
  val build_case_analysis_scheme_default : Environ.env -> Evd.evar_map -> Term.pinductive ->
      Sorts.family -> Evd.evar_map * Term.constr
end

module Logic :
sig
  type refiner_error = Logic.refiner_error =
  | BadType of Term.constr * Term.constr * Term.constr
  | UnresolvedBindings of Names.Name.t list
  | CannotApply of Term.constr * Term.constr
  | NotWellTyped of Term.constr
  | NonLinearProof of Term.constr
  | MetaInType of EConstr.constr
  | IntroNeedsProduct
  | DoesNotOccurIn of Term.constr * Names.Id.t
  | NoSuchHyp of Names.Id.t
  exception RefinerError of refiner_error
  val catchable_exception : exn -> bool
end

module Himsg :
sig
  val explain_refiner_error : Logic.refiner_error -> Pp.std_ppcmds
  val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.std_ppcmds
end

module Extend :
sig
  type ('self, 'a) symbol = ('self, 'a) Extend.symbol
  type 'a user_symbol = 'a Extend.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
end

module Pputils :
sig
  val pr_with_occurrences : ('a -> Pp.std_ppcmds) -> (string -> Pp.std_ppcmds) -> 'a Locus.with_occurrences -> Pp.std_ppcmds
  val pr_red_expr :
    ('a -> Pp.std_ppcmds) * ('a -> Pp.std_ppcmds) * ('b -> Pp.std_ppcmds) * ('c -> Pp.std_ppcmds) ->
    (string -> Pp.std_ppcmds) ->
    ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.std_ppcmds
  val pr_raw_generic : Environ.env -> Genarg.rlevel Genarg.generic_argument -> Pp.std_ppcmds
  val pr_glb_generic : Environ.env -> Genarg.glevel Genarg.generic_argument -> Pp.std_ppcmds
  val pr_or_var : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_var -> Pp.std_ppcmds
  val pr_or_by_notation : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_by_notation -> Pp.std_ppcmds
end

module Ppconstr :
sig
  val pr_name : Names.Name.t -> Pp.std_ppcmds
  [@@ocaml.deprecated "alias of API.Names.Name.print"]

  val pr_id : Names.Id.t -> Pp.std_ppcmds
  val pr_or_var : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_var -> Pp.std_ppcmds
  val pr_with_comments : ?loc:Loc.t -> Pp.std_ppcmds -> Pp.std_ppcmds
  val pr_lident : Names.Id.t Loc.located -> Pp.std_ppcmds
  val pr_lname : Names.Name.t Loc.located -> Pp.std_ppcmds
  val prec_less : int -> int * Ppextend.parenRelation -> bool
  val pr_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds
  val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds
  val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.std_ppcmds
  val pr_lconstr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.std_ppcmds
  val pr_binders : Constrexpr.local_binder_expr list -> Pp.std_ppcmds
  val pr_glob_sort : Misctypes.glob_sort -> Pp.std_ppcmds
end

module Genprint :
sig
  type 'a printer = 'a -> Pp.std_ppcmds
  val generic_top_print : Genarg.tlevel Genarg.generic_argument printer
  val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
                        'raw printer -> 'glb printer -> 'top printer -> unit
end

module Miscprint :
sig
  val pr_or_and_intro_pattern :
    ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_and_intro_pattern_expr -> Pp.std_ppcmds
  val pr_intro_pattern_naming : Misctypes.intro_pattern_naming_expr -> Pp.std_ppcmds
  val pr_intro_pattern :
    ('a -> Pp.std_ppcmds) -> 'a Misctypes.intro_pattern_expr Loc.located -> Pp.std_ppcmds
  val pr_bindings :
    ('a -> Pp.std_ppcmds) ->
    ('a -> Pp.std_ppcmds) -> 'a Misctypes.bindings -> Pp.std_ppcmds
  val pr_bindings_no_with :
    ('a -> Pp.std_ppcmds) ->
    ('a -> Pp.std_ppcmds) -> 'a Misctypes.bindings -> Pp.std_ppcmds
  val pr_with_bindings :
    ('a -> Pp.std_ppcmds) ->
    ('a -> Pp.std_ppcmds) -> 'a * 'a Misctypes.bindings -> Pp.std_ppcmds
end

module Miscops :
sig
  val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
                         ('a,'b,'c) Genredexpr.red_expr_gen -> ('d,'e,'f) Genredexpr.red_expr_gen
  val map_cast_type : ('a -> 'b) -> 'a Misctypes.cast_type -> 'b Misctypes.cast_type
end

module Stateid :
sig
  type t = Stateid.t
  module Self : module type of struct include Stateid.Self end
end

module Stm :
sig
  type state = Stm.state
  val state_of_id :
    Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
end

module Declaremods :
sig
  val append_end_library_hook : (unit -> unit) -> unit
end

module Pfedit :
sig
  val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
  val refine_by_tactic : Environ.env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
                         Term.constr * Evd.evar_map
  val declare_implicit_tactic : unit Proofview.tactic -> unit
  val clear_implicit_tactic : unit -> unit
  val by : unit Proofview.tactic -> bool
  val solve : ?with_end_tac:unit Proofview.tactic ->
      Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
      Proof.proof -> Proof.proof * bool
  val cook_proof :
    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))

  val get_current_context : unit -> Evd.evar_map * Environ.env

  (* Deprecated *)
  val delete_current_proof : unit -> unit
  [@@ocaml.deprecated "use Proof_global.discard_current"]

  val get_current_proof_name : unit -> Names.Id.t
  [@@ocaml.deprecated "use Proof_global.get_current_proof_name"]

end

module Tactics :
sig
  open Proofview

  type change_arg = Pattern.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr
  type tactic_reduction = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
  type elim_scheme = Tactics.elim_scheme =
    {
      elimc: EConstr.constr Misctypes.with_bindings option;
      elimt: EConstr.types;
      indref: Globnames.global_reference option;
      params: EConstr.rel_context;
      nparams: int;
      predicates: EConstr.rel_context;
      npredicates: int;
      branches: EConstr.rel_context;
      nbranches: int;
      args: EConstr.rel_context;
      nargs: int;
      indarg: EConstr.rel_declaration option;
      concl: EConstr.types;
      indarg_in_concl: bool;
      farg_in_concl: bool;
    }

  val unify : ?state:Names.transparent_state -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic
  val intro_then : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
  val reflexivity : unit tactic
  val change_concl : EConstr.constr -> unit tactic
  val apply : EConstr.constr -> unit tactic
  val normalise_vm_in_concl : unit tactic
  val assert_before : Names.Name.t -> EConstr.types -> unit tactic
  val exact_check : EConstr.constr -> unit tactic
  val simplest_elim : EConstr.constr -> unit tactic
  val introf : unit tactic
  val cut : EConstr.types -> unit tactic
  val convert_concl : ?check:bool -> EConstr.types -> Term.cast_kind -> unit tactic
  val intro_using : Names.Id.t -> unit tactic
  val intro : unit tactic
  val fresh_id_in_env : Names.Id.t list -> Names.Id.t -> Environ.env -> Names.Id.t
  val is_quantified_hypothesis : Names.Id.t -> 'a Goal.t -> bool
  val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
  val intro_patterns : bool -> Tactypes.intro_patterns -> unit Proofview.tactic
  val apply_with_delayed_bindings_gen :
    Misctypes.advanced_flag -> Misctypes.evars_flag -> (Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings Loc.located) list -> unit Proofview.tactic
  val apply_delayed_in :
    Misctypes.advanced_flag -> Misctypes.evars_flag -> Names.Id.t -> 
    (Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings Loc.located) list ->
    Tactypes.intro_pattern option -> unit Proofview.tactic
  val elim :
    Misctypes.evars_flag -> Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> EConstr.constr Misctypes.with_bindings option -> unit Proofview.tactic
  val general_case_analysis : Misctypes.evars_flag -> Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings ->  unit Proofview.tactic
  val mutual_fix :
    Names.Id.t -> int -> (Names.Id.t * int * EConstr.constr) list -> int -> unit Proofview.tactic
  val mutual_cofix : Names.Id.t -> (Names.Id.t * EConstr.constr) list -> int -> unit Proofview.tactic
  val forward   : bool -> unit Proofview.tactic option option ->
                  Tactypes.intro_pattern option -> EConstr.constr -> unit Proofview.tactic
  val generalize_gen : (EConstr.constr Locus.with_occurrences * Names.Name.t) list -> unit Proofview.tactic
  val letin_tac : (bool * Tactypes.intro_pattern_naming) option ->
                  Names.Name.t -> EConstr.constr -> EConstr.types option -> Locus.clause -> unit Proofview.tactic
  val letin_pat_tac : Misctypes.evars_flag ->
                      (bool * Tactypes.intro_pattern_naming) option ->
                      Names.Name.t ->
                      Evd.evar_map * EConstr.constr ->
                      Locus.clause -> unit Proofview.tactic
  val induction_destruct : Misctypes.rec_flag -> Misctypes.evars_flag ->
                           (Tactypes.delayed_open_constr_with_bindings Misctypes.destruction_arg
                            * (Tactypes.intro_pattern_naming option * Tactypes.or_and_intro_pattern option)
                            * Locus.clause option) list *
                             EConstr.constr Misctypes.with_bindings option -> unit Proofview.tactic
  val reduce : Redexpr.red_expr -> Locus.clause -> unit Proofview.tactic
  val change : Pattern.constr_pattern option -> change_arg -> Locus.clause -> unit Proofview.tactic
  val intros_reflexivity : unit Proofview.tactic
  val exact_no_check : EConstr.constr -> unit Proofview.tactic
  val assumption : unit Proofview.tactic
  val intros_transitivity : EConstr.constr option -> unit Proofview.tactic
  val vm_cast_no_check : EConstr.constr -> unit Proofview.tactic
  val native_cast_no_check : EConstr.constr -> unit Proofview.tactic
  val case_type : EConstr.types -> unit Proofview.tactic
  val elim_type : EConstr.types -> unit Proofview.tactic
  val cut_and_apply : EConstr.constr -> unit Proofview.tactic
  val left_with_bindings  : Misctypes.evars_flag -> EConstr.constr Misctypes.bindings -> unit Proofview.tactic
  val right_with_bindings : Misctypes.evars_flag -> EConstr.constr Misctypes.bindings -> unit Proofview.tactic
  val any_constructor : Misctypes.evars_flag -> unit Proofview.tactic option -> unit Proofview.tactic
  val constructor_tac : Misctypes.evars_flag -> int option -> int ->
                        EConstr.constr Misctypes.bindings -> unit Proofview.tactic
  val specialize : EConstr.constr Misctypes.with_bindings -> Tactypes.intro_pattern option -> unit Proofview.tactic
  val intros_symmetry : Locus.clause -> unit Proofview.tactic
  val split_with_bindings : Misctypes.evars_flag -> EConstr.constr Misctypes.bindings list -> unit Proofview.tactic
  val intros_until : Misctypes.quantified_hypothesis -> unit Proofview.tactic
  val intro_move : Names.Id.t option -> Names.Id.t Misctypes.move_location -> unit Proofview.tactic
  val move_hyp : Names.Id.t -> Names.Id.t Misctypes.move_location -> unit Proofview.tactic
  val rename_hyp : (Names.Id.t * Names.Id.t) list -> unit Proofview.tactic
  val revert : Names.Id.t list -> unit Proofview.tactic
  val simple_induct : Misctypes.quantified_hypothesis -> unit Proofview.tactic
  val simple_destruct : Misctypes.quantified_hypothesis -> unit Proofview.tactic
  val fix : Names.Id.t option -> int -> unit Proofview.tactic
  val cofix : Names.Id.t option -> unit Proofview.tactic
  val keep : Names.Id.t list -> unit Proofview.tactic
  val clear : Names.Id.t list -> unit Proofview.tactic
  val clear_body : Names.Id.t list -> unit Proofview.tactic
  val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> EConstr.constr  -> unit Proofview.tactic
  val force_destruction_arg : Misctypes.evars_flag -> Environ.env -> Evd.evar_map ->
    Tactypes.delayed_open_constr_with_bindings Misctypes.destruction_arg ->
    Evd.evar_map * EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg
  val apply_with_bindings   : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
  val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Names.Id.t -> unit Proofview.tactic
  val specialize_eqs : Names.Id.t -> unit Proofview.tactic
  val generalize : EConstr.constr list -> unit Proofview.tactic
  val simplest_case : EConstr.constr -> unit Proofview.tactic
  val introduction : ?check:bool -> Names.Id.t -> unit Proofview.tactic
  val convert_concl_no_check : EConstr.types -> Term.cast_kind -> unit Proofview.tactic
  val reduct_in_concl : tactic_reduction * Term.cast_kind -> unit Proofview.tactic
  val reduct_in_hyp : ?check:bool -> tactic_reduction -> Locus.hyp_location -> unit Proofview.tactic
  val convert_hyp_no_check : EConstr.named_declaration -> unit Proofview.tactic
  val reflexivity_red : bool -> unit Proofview.tactic
  val symmetry_red : bool -> unit Proofview.tactic
  val eapply : EConstr.constr -> unit Proofview.tactic
  val transitivity_red : bool -> EConstr.constr option -> unit Proofview.tactic
  val assert_after_replacing : Names.Id.t -> EConstr.types -> unit Proofview.tactic
  val intros : unit Proofview.tactic
  val setoid_reflexivity : unit Proofview.tactic Hook.t
  val setoid_symmetry : unit Proofview.tactic Hook.t
  val setoid_symmetry_in : (Names.Id.t -> unit Proofview.tactic) Hook.t
  val setoid_transitivity : (EConstr.constr option -> unit Proofview.tactic) Hook.t
  val unfold_in_concl :
    (Locus.occurrences * Names.evaluable_global_reference) list -> unit Proofview.tactic
  val intros_using : Names.Id.t list -> unit Proofview.tactic
  val simpl_in_concl : unit Proofview.tactic
  val reduct_option : ?check:bool -> tactic_reduction * Term.cast_kind -> Locus.goal_location -> unit Proofview.tactic
  val simplest_split : unit Proofview.tactic
  val unfold_in_hyp :
    (Locus.occurrences * Names.evaluable_global_reference) list -> Locus.hyp_location -> unit Proofview.tactic
  val split : EConstr.constr Misctypes.bindings -> unit Proofview.tactic
  val red_in_concl : unit Proofview.tactic
  val change_in_concl   : (Locus.occurrences * Pattern.constr_pattern) option -> change_arg -> unit Proofview.tactic
  val eapply_with_bindings  : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
  val assert_by  : Names.Name.t -> EConstr.types -> unit Proofview.tactic ->
                   unit Proofview.tactic
  val intro_avoiding : Names.Id.t list -> unit Proofview.tactic
  val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic
  val pattern_option :  (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic
  val compute_elim_sig : Evd.evar_map -> ?elimc:EConstr.constr Misctypes.with_bindings -> EConstr.types -> elim_scheme
  val try_intros_until :
    (Names.Id.t -> unit Proofview.tactic) -> Misctypes.quantified_hypothesis -> unit Proofview.tactic
  val cache_term_by_tactic_then :
    opaque:bool -> ?goal_type:(EConstr.constr option) -> Names.Id.t ->
    Decl_kinds.goal_kind -> unit Proofview.tactic -> (EConstr.constr -> EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tactic
  val apply_type : EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
  val hnf_in_concl : unit Proofview.tactic
  val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic

  module New :
  sig
    val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
    val reduce_after_refine : unit Proofview.tactic
  end
  module Simple :
  sig
    val intro : Names.Id.t -> unit Proofview.tactic
    val apply  : EConstr.constr -> unit Proofview.tactic
    val case : EConstr.constr -> unit Proofview.tactic
  end
end

module Tacticals :
sig
  open Proof_type
  val tclORELSE        : tactic -> tactic -> tactic
  val tclDO : int -> tactic -> tactic
  val tclIDTAC : tactic
  val tclFAIL : int -> Pp.std_ppcmds -> tactic
  val tclTHEN : tactic -> tactic -> tactic
  val tclTHENLIST      : tactic list -> tactic
  val pf_constr_of_global :         
    Globnames.global_reference -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic
  val tclMAP : ('a -> tactic) -> 'a list -> tactic
  val tclTRY           : tactic -> tactic
  val tclCOMPLETE      : tactic -> tactic
  val tclTHENS : tactic -> tactic list -> tactic
  val tclFIRST         : tactic list -> tactic
  val tclTHENFIRST     : tactic -> tactic -> tactic
  val tclTHENLAST      : tactic -> tactic -> tactic
  val tclTHENSFIRSTn   : tactic -> tactic array -> tactic -> tactic
  val tclTHENSLASTn    : tactic -> tactic -> tactic array -> tactic
  val tclSOLVE         : tactic list -> tactic

  val onClause   : (Names.Id.t option -> tactic) -> Locus.clause -> tactic
  val onAllHypsAndConcl : (Names.Id.t option -> tactic) -> tactic
  val onLastHypId : (Names.Id.t -> tactic) -> tactic
  val onNthHypId : int -> (Names.Id.t -> tactic) -> tactic
  val onNLastHypsId : int -> (Names.Id.t list -> tactic) -> tactic

  val tclTHENSEQ : tactic list -> tactic
  [@@ocaml.deprecated "alias of API.Tacticals.tclTHENLIST"]

  val nLastDecls : int -> Proof_type.goal Evd.sigma -> EConstr.named_context

  val tclTHEN_i : tactic -> (int -> tactic) -> tactic

  val tclPROGRESS : tactic -> tactic

  val elimination_sort_of_goal : Proof_type.goal Evd.sigma -> Sorts.family

  module New :
  sig
    open Proofview
    val tclORELSE0 : unit tactic -> unit tactic -> unit tactic
    val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic
    val pf_constr_of_global : Globnames.global_reference -> EConstr.constr tactic
    val tclTHEN : unit tactic -> unit tactic -> unit tactic
    val tclTHENS : unit tactic -> unit tactic list -> unit tactic
    val tclFIRST : unit tactic list -> unit tactic
    val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic
    val tclORELSE  : unit tactic -> unit tactic -> unit tactic
    val tclREPEAT : unit tactic -> unit tactic
    val tclTRY : unit tactic -> unit tactic
    val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic
    val tclPROGRESS :  unit Proofview.tactic -> unit Proofview.tactic
    val tclTHENS3PARTS : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic
    val tclDO : int -> unit tactic -> unit tactic
    val tclTIMEOUT : int -> unit tactic -> unit tactic
    val tclTIME : string option -> 'a tactic -> 'a tactic
    val tclOR : unit tactic -> unit tactic -> unit tactic
    val tclONCE : unit tactic -> unit tactic
    val tclEXACTLY_ONCE : unit tactic -> unit tactic
    val tclIFCATCH :
      unit tactic  ->
      (unit -> unit tactic) ->
      (unit -> unit tactic) -> unit tactic
    val tclSOLVE : unit tactic list -> unit tactic
    val tclCOMPLETE : 'a tactic -> 'a tactic
    val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic
    val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
    val tclDELAYEDWITHHOLES : bool -> 'a Tactypes.delayed_open -> ('a -> unit tactic) -> unit tactic
    val tclTHENLIST : unit tactic list -> unit tactic
    val tclTHENLAST  : unit tactic -> unit tactic -> unit tactic
    val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic
    val tclIDTAC : unit tactic
    val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic
    val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic
  end
end

module Equality :
sig
  type orientation = bool
  type freeze_evars_flag = bool
  type dep_proof_flag = bool
  type conditions =
    | Naive
    | FirstSolved
    | AllMatches

  val build_selector :
    Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types ->
    EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr
  val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
  val general_rewrite :
    orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
    ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
  val inj : Tactypes.intro_patterns option -> Misctypes.evars_flag ->
            Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
  val general_multi_rewrite :
    Misctypes.evars_flag -> (bool * Misctypes.multi * Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings) list ->
    Locus.clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
  val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
  val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic
  val dEq : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
  val discr_tac : Misctypes.evars_flag ->
                  EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
  val injClause    : Tactypes.intro_patterns option -> Misctypes.evars_flag ->
                     EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic

  val simpleInjClause : Misctypes.evars_flag ->
                        EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option ->
                        unit Proofview.tactic
  val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
  val rewriteInHyp : bool -> EConstr.constr -> Names.Id.t -> unit Proofview.tactic
  val cutRewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
  val cutRewriteInHyp : bool -> EConstr.types -> Names.Id.t -> unit Proofview.tactic
  val general_rewrite_ebindings_clause : Names.Id.t option ->
                                         orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
                                         ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic
  val subst : Names.Id.t list -> unit Proofview.tactic
  type subst_tactic_flags = Equality.subst_tactic_flags = {
    only_leibniz : bool;
    rewrite_dependent_proof : bool
  }
  val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic

  val general_rewrite_in :
    orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> 
    ?tac:(unit Proofview.tactic * conditions) -> Names.Id.t -> EConstr.constr -> Misctypes.evars_flag -> unit Proofview.tactic

  val general_setoid_rewrite_clause :
  (Names.Id.t option -> orientation -> Locus.occurrences -> EConstr.constr Misctypes.with_bindings ->
   new_goals:EConstr.constr list -> unit Proofview.tactic) Hook.t

  val discrConcl   : unit Proofview.tactic
  val rewriteLR : ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
  val rewriteRL : ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr  -> unit Proofview.tactic
  val general_rewrite_bindings :
    orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
    ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic
  val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
  val discrHyp : Names.Id.t -> unit Proofview.tactic
  val injectable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
  val injHyp : Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic
  val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic
end

module Contradiction :
sig
  val contradiction : EConstr.constr Misctypes.with_bindings option -> unit Proofview.tactic
  val absurd : EConstr.constr -> unit Proofview.tactic
end

module Clenv :
sig
  type hole = Clenv.hole = {
        hole_evar : EConstr.constr;
        hole_type : EConstr.types;
        hole_deps  : bool;
        hole_name : Names.Name.t;
      }
  type clause = Clenv.clause = {
        cl_holes : hole list;
        cl_concl : EConstr.types;
      }
  val make_evar_clause : Environ.env -> Evd.evar_map -> ?len:int -> EConstr.types ->
                         (Evd.evar_map * clause)
  val solve_evar_clause : Environ.env -> Evd.evar_map -> bool -> clause -> EConstr.constr Misctypes.bindings ->
                          Evd.evar_map
  type clausenv = Clenv.clausenv
  val pr_clenv : Clenv.clausenv -> Pp.std_ppcmds
end

module Hints :
sig
  type hint = Hints.hint
  type debug = Hints.debug =
             | Debug | Info | Off
  type 'a hints_path_atom_gen = 'a Hints.hints_path_atom_gen =
    | PathHints of 'a list
    | PathAny
  type hint_term = Hints.hint_term =
    | IsGlobRef of Globnames.global_reference
    | IsConstr of EConstr.constr * Univ.ContextSet.t
  type hint_db_name = string
  type hint_info = (Names.Id.t list * Pattern.constr_pattern) Vernacexpr.hint_info_gen
  type hnf = bool
  type hints_path_atom = Globnames.global_reference hints_path_atom_gen

  type 'a hints_path_gen = 'a Hints.hints_path_gen =
    | PathAtom of 'a hints_path_atom_gen
    | PathStar of 'a hints_path_gen
    | PathSeq of 'a hints_path_gen * 'a hints_path_gen
    | PathOr of 'a hints_path_gen * 'a hints_path_gen
    | PathEmpty
    | PathEpsilon

  type hints_path = Globnames.global_reference hints_path_gen

  type hints_entry = Hints.hints_entry =
    | HintsResolveEntry of (hint_info * Decl_kinds.polymorphic * hnf * hints_path_atom * hint_term) list
    | HintsImmediateEntry of (hints_path_atom * Decl_kinds.polymorphic * hint_term) list
    | HintsCutEntry of hints_path
    | HintsUnfoldEntry of Names.evaluable_global_reference list
    | HintsTransparencyEntry of Names.evaluable_global_reference list * bool
    | HintsModeEntry of Globnames.global_reference * Vernacexpr.hint_mode list
    | HintsExternEntry of hint_info * Genarg.glob_generic_argument

  type 'a hint_ast = 'a Hints.hint_ast =
    | Res_pf     of 'a
    | ERes_pf    of 'a
    | Give_exact of 'a
    | Res_pf_THEN_trivial_fail of 'a
    | Unfold_nth of Names.evaluable_global_reference
    | Extern     of Genarg.glob_generic_argument
  type raw_hint = EConstr.constr * EConstr.types * Univ.ContextSet.t
  type 'a with_metadata = 'a Hints.with_metadata = private {
      pri     : int;
      poly    : Decl_kinds.polymorphic;
      pat     : Pattern.constr_pattern option;
      name    : hints_path_atom;
      db : string option;
      secvars : Names.Id.Pred.t;
      code    : 'a;
    }
  type full_hint = hint with_metadata

  module Hint_db :
  sig
    type t = Hints.Hint_db.t
    val empty : ?name:hint_db_name -> Names.transparent_state -> bool -> t
    val transparent_state : t -> Names.transparent_state
    val iter : (Globnames.global_reference option ->
                Vernacexpr.hint_mode array list -> full_hint list -> unit) -> t -> unit
  end
  type hint_db = Hint_db.t

  val add_hints : Vernacexpr.locality_flag -> hint_db_name list -> hints_entry -> unit
  val searchtable_map : hint_db_name -> hint_db
  val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds
  val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds
  val glob_hints_path_atom :
    Prelude.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
  val pp_hints_path : hints_path -> Pp.std_ppcmds
  val glob_hints_path :
    Prelude.reference hints_path_gen -> Globnames.global_reference hints_path_gen
  val typeclasses_db : hint_db_name
  val add_hints_init : (unit -> unit) -> unit
  val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit
  val empty_hint_info : 'a Vernacexpr.hint_info_gen
  val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast
  val pr_hint_db : Hint_db.t -> Pp.std_ppcmds
end

module Auto :
sig
  val default_auto : unit Proofview.tactic
  val full_trivial : ?debug:Hints.debug ->
                     Tactypes.delayed_open_constr list -> unit Proofview.tactic
  val h_auto   : ?debug:Hints.debug ->
                 int option -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
  val h_trivial : ?debug:Hints.debug ->
                  Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
  val new_full_auto : ?debug:Hints.debug ->
                      int -> Tactypes.delayed_open_constr list -> unit Proofview.tactic
  val full_auto : ?debug:Hints.debug ->
                  int -> Tactypes.delayed_open_constr list -> unit Proofview.tactic
  val new_auto : ?debug:Hints.debug ->
                 int -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list -> unit Proofview.tactic
  val default_full_auto : unit Proofview.tactic
end

module Hipattern :
sig
  exception NoEquationFound
  type 'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option
  type testing_function = Evd.evar_map -> EConstr.constr -> bool
  val is_disjunction : ?strict:bool -> ?onlybinary:bool -> testing_function
  val match_with_disjunction : ?strict:bool -> ?onlybinary:bool -> (EConstr.constr * EConstr.constr list) matching_function
  val match_with_equality_type : (EConstr.constr * EConstr.constr list) matching_function
  val is_empty_type : testing_function
  val is_unit_type : testing_function
  val is_unit_or_eq_type : testing_function
  val is_conjunction : ?strict:bool -> ?onlybinary:bool -> testing_function
  val match_with_conjunction : ?strict:bool -> ?onlybinary:bool -> (EConstr.constr * EConstr.constr list) matching_function
  val match_with_imp_term : (EConstr.constr * EConstr.constr) matching_function
  val match_with_forall_term : (Names.Name.t * EConstr.constr * EConstr.constr) matching_function
  val match_with_nodep_ind : (EConstr.constr * EConstr.constr list * int) matching_function
  val match_with_sigma_type : (EConstr.constr * EConstr.constr list) matching_function
end

module Inv :
sig
  val dinv :
    Misctypes.inversion_kind -> EConstr.constr option ->
    Tactypes.or_and_intro_pattern option -> Misctypes.quantified_hypothesis -> unit Proofview.tactic
  val inv_clause :
    Misctypes.inversion_kind -> Tactypes.or_and_intro_pattern option -> Names.Id.t list ->
    Misctypes.quantified_hypothesis -> unit Proofview.tactic
  val inv_clear_tac : Names.Id.t -> unit Proofview.tactic
  val inv_tac : Names.Id.t -> unit Proofview.tactic
  val dinv_tac : Names.Id.t -> unit Proofview.tactic
  val dinv_clear_tac : Names.Id.t -> unit Proofview.tactic
  val inv : Misctypes.inversion_kind -> Tactypes.or_and_intro_pattern option ->
            Misctypes.quantified_hypothesis -> unit Proofview.tactic
end

module Leminv :
sig
  val lemInv_clause :
    Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic
  val add_inversion_lemma_exn :
    Names.Id.t -> Constrexpr.constr_expr -> Misctypes.glob_sort -> bool -> (Names.Id.t -> unit Proofview.tactic) ->
    unit
end

module Vernacentries :
sig
  val dump_global : Prelude.reference Misctypes.or_by_notation -> unit
  val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
                            Evd.evar_map * Redexpr.red_expr) Hook.t
  val command_focus : unit Proof.focus_kind
end

module Evar_refiner :
sig
  val w_refine : Evar.t * Evd.evar_info ->
                 Pretyping.glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map
end

module Obligations :
sig
  val default_tactic : unit Proofview.tactic ref
  val obligation : int * Names.Id.t option * Constrexpr.constr_expr option ->
                   Genarg.glob_generic_argument option -> unit
  val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> unit
  val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit
  val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit
  val solve_all_obligations : unit Proofview.tactic option -> unit
  val admit_obligations : Names.Id.t option -> unit
  val show_obligations : ?msg:bool -> Names.Id.t option -> unit
  val show_term : Names.Id.t option -> Pp.std_ppcmds
end

module Elim :
sig
  val h_decompose : Names.inductive list -> EConstr.constr -> unit Proofview.tactic
  val h_double_induction : Misctypes.quantified_hypothesis -> Misctypes.quantified_hypothesis-> unit Proofview.tactic
  val h_decompose_or : EConstr.constr -> unit Proofview.tactic
  val h_decompose_and : EConstr.constr -> unit Proofview.tactic
end

module Redops :
sig
  val all_flags : 'a Genredexpr.glob_red_flag
  val make_red_flag : 'a Genredexpr.red_atom list -> 'a Genredexpr.glob_red_flag
end

module Autorewrite :
sig
  type rew_rule = { rew_lemma: Term.constr;
                    rew_type: Term.types;
                    rew_pat: Term.constr;
                    rew_ctx: Univ.ContextSet.t;
                    rew_l2r: bool;
                    rew_tac: Genarg.glob_generic_argument option }
  type raw_rew_rule = (Term.constr Univ.in_universe_context_set * bool *
                         Genarg.raw_generic_argument option)
                        Loc.located
  val auto_multi_rewrite : ?conds:Equality.conditions -> string list -> Locus.clause -> unit Proofview.tactic
  val auto_multi_rewrite_with : ?conds:Equality.conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
  val add_rew_rules : string -> raw_rew_rule list -> unit
  val find_rewrites : string -> rew_rule list
  val find_matches : string -> Term.constr -> rew_rule list
  val print_rewrite_hintdb : string -> Pp.std_ppcmds
end

module Refine :
sig
  val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic
  val solve_constraints : unit Proofview.tactic
end

module Find_subterm :
sig
  val error_invalid_occurrence : int list -> 'a
end

module Vernac_classifier :
sig
  val declare_vernac_classifier :
    Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> Vernacexpr.vernac_classification) -> unit
  val classify_as_proofstep : Vernacexpr.vernac_classification
  val classify_as_query : Vernacexpr.vernac_classification
  val classify_as_sideeff : Vernacexpr.vernac_classification
  val classify_vernac : Vernacexpr.vernac_expr -> Vernacexpr.vernac_classification
end

module Keys :
sig
  type key = Keys.key
  val constr_key : ('a -> ('a, 't, 'u, 'i) Term.kind_of_term) -> 'a -> key option
  val declare_equiv_keys : key -> key -> unit
  val pr_keys : (Globnames.global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds
end

module Eauto :
sig
  val e_assumption : unit Proofview.tactic
  val e_give_exact : ?flags:Unification.unify_flags -> EConstr.constr -> unit Proofview.tactic
  val prolog_tac : Tactypes.delayed_open_constr list -> int -> unit Proofview.tactic
  val make_dimension : int option -> int option -> bool * int
  val gen_eauto : ?debug:Hints.debug -> bool * int -> Tactypes.delayed_open_constr list ->
                  Hints.hint_db_name list option -> unit Proofview.tactic
  val autounfold_tac : Hints.hint_db_name list option -> Locus.clause -> unit Proofview.tactic
  val autounfold_one : Hints.hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic
  val eauto_with_bases :
    ?debug:Hints.debug -> bool * int -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> Proof_type.tactic
end

module Class_tactics :
sig
  type search_strategy = Class_tactics.search_strategy =
    | Dfs
    | Bfs
  val set_typeclasses_debug : bool -> unit
  val set_typeclasses_strategy : search_strategy -> unit
  val set_typeclasses_depth : int option -> unit
  val typeclasses_eauto : ?only_classes:bool -> ?st:Names.transparent_state -> ?strategy:search_strategy ->
                        depth:(Int.t option) ->
                        Hints.hint_db_name list -> unit Proofview.tactic
  val head_of_constr : Names.Id.t -> EConstr.constr -> unit Proofview.tactic
  val not_evar : EConstr.constr -> unit Proofview.tactic
  val is_ground : EConstr.constr -> unit Proofview.tactic
  val autoapply : EConstr.constr -> Hints.hint_db_name -> unit Proofview.tactic
  val catchable : exn -> bool
end

module Ind_tables :
sig
  type individual = Ind_tables.individual
  type 'a scheme_kind = 'a Ind_tables.scheme_kind

  val check_scheme : 'a scheme_kind -> Names.inductive -> bool
  val find_scheme : ?mode:Declare.internal_flag -> 'a scheme_kind -> Names.inductive -> Names.Constant.t * Safe_typing.private_constants
  val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds
end

module Elimschemes :
sig
  val case_scheme_kind_from_prop : Ind_tables.individual Ind_tables.scheme_kind
  val case_dep_scheme_kind_from_type_in_prop : Ind_tables.individual Ind_tables.scheme_kind
  val case_scheme_kind_from_type : Ind_tables.individual Ind_tables.scheme_kind
  val case_dep_scheme_kind_from_type : Ind_tables.individual Ind_tables.scheme_kind
  val case_dep_scheme_kind_from_prop : Ind_tables.individual Ind_tables.scheme_kind
end

module Lemmas :
sig
  type 'a declaration_hook = 'a Lemmas.declaration_hook
  val mk_hook :
    (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
  val start_proof : Names.Id.t -> ?pl:Proof_global.universe_binders -> Decl_kinds.goal_kind -> Evd.evar_map ->
    ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
    ?sign:Environ.named_context_val -> EConstr.types ->
    ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
    unit declaration_hook -> unit
  val call_hook :
    Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
  val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
  val get_current_context : unit -> Evd.evar_map * Environ.env
end

module Eqdecide :
sig
  val compare : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
  val decideEqualityGoal : unit Proofview.tactic
end

module Locusops :
sig
  val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool
  val nowhere : 'a Locus.clause_expr
  val allHypsAndConcl : 'a Locus.clause_expr
  val is_nowhere : 'a Locus.clause_expr -> bool
  val occurrences_map :
    ('a list -> 'b list) -> 'a Locus.occurrences_gen -> 'b Locus.occurrences_gen
  val convert_occs : Locus.occurrences -> bool * int list
  val onConcl : 'a Locus.clause_expr
  val onHyp : 'a -> 'a Locus.clause_expr
end

module Topfmt :
sig
  val std_ft : Format.formatter ref
  val with_output_to : out_channel -> Format.formatter
  val get_margin : unit -> int option
end

module Nameops :
sig
  val atompart_of_id : Names.Id.t -> string

  val pr_id : Names.Id.t -> Pp.std_ppcmds
  [@@ocaml.deprecated "alias of API.Names.Id.print"]

  val pr_name : Names.Name.t -> Pp.std_ppcmds
  [@@ocaml.deprecated "alias of API.Names.Name.print"]

  val name_fold : (Names.Id.t -> 'a -> 'a) -> Names.Name.t -> 'a -> 'a
  val name_app : (Names.Id.t -> Names.Id.t) -> Names.Name.t -> Names.Name.t
  val add_suffix : Names.Id.t -> string -> Names.Id.t
  val increment_subscript : Names.Id.t -> Names.Id.t
  val make_ident : string -> int option -> Names.Id.t
  val out_name : Names.Name.t -> Names.Id.t
  val pr_lab : Names.Label.t -> Pp.std_ppcmds
  module Name :
  sig
    include module type of struct include Names.Name end
    val get_id : t -> Names.Id.t
    val fold_right : (Names.Id.t -> 'a -> 'a) -> t -> 'a -> 'a
  end
end

module Declareops :
sig
  val constant_has_body : Declarations.constant_body -> bool
  val is_opaque : Declarations.constant_body -> bool
  val eq_recarg : Declarations.recarg -> Declarations.recarg -> bool
  val body_of_constant :
    Opaqueproof.opaquetab -> Declarations.constant_body -> Term.constr option
end

module Constr :
sig
  type t = Term.constr
  [@@ocaml.deprecated "alias of API.Term.constr"]

  type constr = Term.constr
  [@@ocaml.deprecated "alias of API.Term.constr"]

  type types = Term.constr
  [@@ocaml.deprecated "alias of API.Term.types"]

  type cast_kind = Term.cast_kind =
                 | VMcast
                 | NATIVEcast
                 | DEFAULTcast
                 | REVERTcast
  type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Term.kind_of_term =
     | Rel       of int
     | Var       of Names.Id.t
     | Meta      of Term.metavariable
     | Evar      of 'constr Term.pexistential
     | Sort      of 'sort
     | Cast      of 'constr * cast_kind * 'types
     | Prod      of Names.Name.t * 'types * 'types
     | Lambda    of Names.Name.t * 'types * 'constr
     | LetIn     of Names.Name.t * 'constr * 'types * 'constr
     | App       of 'constr * 'constr array
     | Const     of (Names.Constant.t * 'univs)
     | Ind       of (Names.inductive * 'univs)
     | Construct of (Names.constructor * 'univs)
     | Case      of Term.case_info * 'constr * 'constr * 'constr array
     | Fix       of ('constr, 'types) Term.pfixpoint
     | CoFix     of ('constr, 'types) Term.pcofixpoint
     | Proj      of Names.Projection.t * 'constr
  [@@ocaml.deprecated "alias of API.Term.cast_kind"]

  val equal : Term.constr -> Term.constr -> bool
  [@@ocaml.deprecated "alias of API.Term.eq_constr"]

  val mkIndU : Term.pinductive -> Term.constr
  [@@ocaml.deprecated "alias of API.Term.mkIndU"]

  val mkConstU : Term.pconstant -> Term.constr
  [@@ocaml.deprecated "alias of API.Term.mkConstU"]

  val mkConst : Names.Constant.t -> Term.constr
  [@@ocaml.deprecated "alias of API.Term.mkConst"]

  val mkVar : Names.Id.t -> Term.constr
  [@@ocaml.deprecated "alias of API.Term.mkVar"]

  val compare : Term.constr -> Term.constr -> int
  [@@ocaml.deprecated "alias of API.Term.constr_ord"]

  val mkApp : Term.constr * Term.constr array -> Term.constr
  [@@ocaml.deprecated "alias of API.Term.mkApp"]
end
[@@ocaml.deprecated "alias of API.Term"]

module Coq_config :
sig
  val exec_extension : string
end

module Kindops :
sig
  val logical_kind_of_goal_kind : Decl_kinds.goal_object_kind -> Decl_kinds.logical_kind
end

module States :
sig
  val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b
  val with_state_protection : ('a -> 'b) -> 'a -> 'b
end

module Command :
sig
  type structured_fixpoint_expr = Command.structured_fixpoint_expr
  type recursive_preentry = Names.Id.t list * Term.constr option list * Term.types list
  type structured_inductive_expr = Command.structured_inductive_expr
  type one_inductive_impls = Command.one_inductive_impls

  val do_mutual_inductive :
    (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.polymorphic -> 
    Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit

  val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option ->
    Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr ->
    Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit

  val do_fixpoint :
    Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit

  val extract_fixpoint_components : bool ->
    (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
    structured_fixpoint_expr list * Vernacexpr.decl_notation list

  val interp_fixpoint :
    structured_fixpoint_expr list -> Vernacexpr.decl_notation list ->
    recursive_preentry * Vernacexpr.lident list option * UState.t * 
      (EConstr.rel_context * Impargs.manual_implicits * int option) list

  val extract_mutual_inductive_declaration_components :
    (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list ->
    structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list

  val interp_mutual_inductive :
    structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.polymorphic ->
    Decl_kinds.private_flag -> Decl_kinds.recursivity_kind ->
    Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list

  val declare_mutual_inductive_with_eliminations :
    Entries.mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
    Names.MutInd.t
end

module Ppvernac :
sig
  val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
  val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
end

module Topconstr :
sig
  val replace_vars_constr_expr :
  Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr
end