diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 1 | ||||
| -rw-r--r-- | API/API.mli | 691 |
2 files changed, 497 insertions, 195 deletions
diff --git a/API/API.ml b/API/API.ml index 9a67e3111f..378c03ee4f 100644 --- a/API/API.ml +++ b/API/API.ml @@ -271,6 +271,7 @@ module Command = Command module Classes = Classes (* module Record *) (* module Assumptions *) +module Vernacstate = Vernacstate module Vernacinterp = Vernacinterp module Mltop = Mltop module Topfmt = Topfmt diff --git a/API/API.mli b/API/API.mli index d0564f9ec2..e320e496c0 100644 --- a/API/API.mli +++ b/API/API.mli @@ -83,6 +83,7 @@ sig val repr : t -> Id.t list val equal : t -> t -> bool val to_string : t -> string + val print : t -> Pp.t end module MBId : sig @@ -300,21 +301,31 @@ sig [@@ocaml.deprecated "alias of API.Names.Constant.make3"] val debug_pr_con : Constant.t -> Pp.t + [@@ocaml.deprecated "Alias of Names"] val debug_pr_mind : MutInd.t -> Pp.t + [@@ocaml.deprecated "Alias of Names"] val pr_con : Constant.t -> Pp.t + [@@ocaml.deprecated "Alias of Names"] val string_of_con : Constant.t -> string + [@@ocaml.deprecated "Alias of Names"] val string_of_mind : MutInd.t -> string + [@@ocaml.deprecated "Alias of Names"] val debug_string_of_mind : MutInd.t -> string + [@@ocaml.deprecated "Alias of Names"] val debug_string_of_con : Constant.t -> string + [@@ocaml.deprecated "Alias of Names"] type identifier = Id.t - module Idset : Set.S with type elt = identifier and type t = Id.Set.t + [@@ocaml.deprecated "Alias of Names"] + + module Idset : Set.S with type elt = Id.t and type t = Id.Set.t + [@@ocaml.deprecated "Alias of Id.Set.t"] end @@ -329,10 +340,11 @@ sig end type universe_level = Level.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module LSet : sig - include CSig.SetS with type elt = universe_level + include CSig.SetS with type elt = Level.t val pr : (Level.t -> Pp.t) -> t -> Pp.t end @@ -343,6 +355,7 @@ sig end type universe = Universe.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module Instance : sig @@ -359,7 +372,7 @@ sig type constraint_type = Lt | Le | Eq - type univ_constraint = universe_level * constraint_type * universe_level + type univ_constraint = Level.t * constraint_type * Level.t module Constraint : sig include Set.S with type elt = univ_constraint @@ -374,6 +387,7 @@ sig end type universe_context = UContext.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module AUContext : sig @@ -382,6 +396,7 @@ sig end type abstract_universe_context = AUContext.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module CumulativityInfo : sig @@ -389,12 +404,14 @@ sig end type cumulativity_info = CumulativityInfo.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module ACumulativityInfo : sig type t end type abstract_cumulativity_info = ACumulativityInfo.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module ContextSet : sig @@ -408,14 +425,16 @@ sig type 'a in_universe_context = 'a * UContext.t type universe_context_set = ContextSet.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] type universe_set = LSet.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t module LMap : sig - include CMap.ExtS with type key = universe_level and module Set := LSet + include CMap.ExtS with type key = Level.t and module Set := LSet val union : 'a t -> 'a t -> 'a t val diff : 'a t -> 'a t -> 'a t @@ -424,8 +443,8 @@ sig end type 'a universe_map = 'a LMap.t - type universe_subst = universe universe_map - type universe_level_subst = universe_level universe_map + type universe_subst = Universe.t universe_map + type universe_level_subst = Level.t universe_map val enforce_leq : Universe.t constraint_function val pr_uni : Universe.t -> Pp.t @@ -459,6 +478,7 @@ sig type family = InProp | InSet | InType val family : t -> family + val univ_of_sort : t -> Univ.Universe.t end module Evar : @@ -471,6 +491,8 @@ sig val equal : t -> t -> bool + val print : t -> Pp.t + (** a set of unique identifiers of some {i evars} *) module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set @@ -479,6 +501,7 @@ end module Constr : sig + open Names type t @@ -495,12 +518,16 @@ sig type metavariable = int type existential_key = Evar.t - type 'constr pexistential = existential_key * 'constr array + [@@ocaml.deprecated "use Evar.t"] + + type 'constr pexistential = Evar.t * 'constr array type 'a puniverses = 'a Univ.puniverses - type pconstant = Constant.t puniverses - type pinductive = inductive puniverses - type pconstructor = constructor puniverses + [@@ocaml.deprecated "use Univ.puniverses"] + + type pconstant = Constant.t Univ.puniverses + type pinductive = inductive Univ.puniverses + type pconstructor = constructor Univ.puniverses type ('constr, 'types) prec_declaration = Name.t array * 'types array * 'constr array @@ -556,13 +583,13 @@ sig val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr -val map_with_binders : - ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr -val map : (constr -> constr) -> constr -> constr + val map_with_binders : + ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr + val map : (constr -> constr) -> constr -> constr -val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a -val iter : (constr -> unit) -> constr -> unit -val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool + val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a + val iter : (constr -> unit) -> constr -> unit + val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool val equal : t -> t -> bool val eq_constr_nounivs : t -> t -> bool @@ -573,7 +600,7 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool val mkRel : int -> t val mkVar : Id.t -> t val mkMeta : metavariable -> t - type existential = existential_key * constr array + type existential = Evar.t * constr array val mkEvar : existential -> t val mkSort : Sorts.t -> t val mkProp : t @@ -584,7 +611,11 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool val mkLambda : Name.t * types * t -> t val mkLetIn : Name.t * t * types * t -> t val mkApp : t * t array -> t - val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses + val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses + + type rec_declaration = Name.t array * types array * constr array + type fixpoint = (int array * int) * rec_declaration + val mkFix : fixpoint -> constr val mkConst : Constant.t -> t val mkConstU : pconstant -> t @@ -600,6 +631,109 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool val mkCase : case_info * t * t * t array -> t + (** {6 Simple case analysis} *) + val isRel : constr -> bool + val isRelN : int -> constr -> bool + val isVar : constr -> bool + val isVarId : Id.t -> constr -> bool + val isInd : constr -> bool + val isEvar : constr -> bool + val isMeta : constr -> bool + val isEvar_or_Meta : constr -> bool + val isSort : constr -> bool + val isCast : constr -> bool + val isApp : constr -> bool + val isLambda : constr -> bool + val isLetIn : constr -> bool + val isProd : constr -> bool + val isConst : constr -> bool + val isConstruct : constr -> bool + val isFix : constr -> bool + val isCoFix : constr -> bool + val isCase : constr -> bool + val isProj : constr -> bool + + val is_Prop : constr -> bool + val is_Set : constr -> bool + val isprop : constr -> bool + val is_Type : constr -> bool + val iskind : constr -> bool + val is_small : Sorts.t -> bool + + (** {6 Term destructors } *) + (** Destructor operations are partial functions and + @raise DestKO if the term has not the expected form. *) + + exception DestKO + + (** Destructs a de Bruijn index *) + val destRel : constr -> int + + (** Destructs an existential variable *) + val destMeta : constr -> metavariable + + (** Destructs a variable *) + val destVar : constr -> Id.t + + (** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether + [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) + val destSort : constr -> Sorts.t + + (** Destructs a casted term *) + val destCast : constr -> constr * cast_kind * constr + + (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) + val destProd : types -> Name.t * types * types + + (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) + val destLambda : constr -> Name.t * types * constr + + (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) + val destLetIn : constr -> Name.t * constr * types * constr + + (** Destructs an application *) + val destApp : constr -> constr * constr array + + (** Decompose any term as an applicative term; the list of args can be empty *) + val decompose_app : constr -> constr * constr list + + (** Same as [decompose_app], but returns an array. *) + val decompose_appvect : constr -> constr * constr array + + (** Destructs a constant *) + val destConst : constr -> Constant.t Univ.puniverses + + (** Destructs an existential variable *) + val destEvar : constr -> existential + + (** Destructs a (co)inductive type *) + val destInd : constr -> inductive Univ.puniverses + + (** Destructs a constructor *) + val destConstruct : constr -> constructor Univ.puniverses + + (** Destructs a [match c as x in I args return P with ... | + Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args + return P in t1], or [if c then t1 else t2]) + @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] + where [info] is pretty-printing information *) + val destCase : constr -> case_info * constr * constr * constr array + + (** Destructs a projection *) + val destProj : constr -> Projection.t * constr + + (** Destructs the {% $ %}i{% $ %}th function of the block + [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} + with f{_ 2} ctx{_ 2} = b{_ 2} + ... + with f{_ n} ctx{_ n} = b{_ n}], + where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. + *) + val destFix : constr -> fixpoint + + type cofixpoint = int * rec_declaration + val destCoFix : constr -> cofixpoint + end module Context : @@ -830,67 +964,81 @@ end module Term : sig + open Constr type sorts_family = Sorts.family = InProp | InSet | InType + [@@ocaml.deprecated "Alias of Sorts.family"] type contents = Sorts.contents = Pos | Null + [@@ocaml.deprecated "Alias of Sorts.contents"] type sorts = Sorts.t = - | Prop of contents + | Prop of Sorts.contents | Type of Univ.Universe.t [@@ocaml.deprecated "alias of API.Sorts.t"] - type constr = Constr.t - type types = Constr.t - type metavariable = int + [@@ocaml.deprecated "Alias of Constr.metavariable"] type ('constr, 'types) prec_declaration = Names.Name.t array * 'types array * 'constr array + [@@ocaml.deprecated "Alias of Constr.prec_declaration"] type 'constr pexistential = 'constr Constr.pexistential + [@@ocaml.deprecated "Alias of Constr.pexistential"] + type cast_kind = Constr.cast_kind = | VMcast | NATIVEcast | DEFAULTcast | REVERTcast + [@@ocaml.deprecated "Alias of Constr.cast_kind"] type 'a puniverses = 'a Univ.puniverses - type pconstant = Names.Constant.t puniverses - type pinductive = Names.inductive puniverses - type pconstructor = Names.constructor puniverses + [@@ocaml.deprecated "Alias of Constr.puniverses"] + type pconstant = Names.Constant.t Univ.puniverses + [@@ocaml.deprecated "Alias of Constr.pconstant"] + type pinductive = Names.inductive Univ.puniverses + [@@ocaml.deprecated "Alias of Constr.pinductive"] + type pconstructor = Names.constructor Univ.puniverses + [@@ocaml.deprecated "Alias of Constr.pconstructor"] type case_style = Constr.case_style = | LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle + [@@ocaml.deprecated "Alias of Constr.case_style"] type case_printing = Constr.case_printing = { ind_tags : bool list; cstr_tags : bool list array; - style : case_style + style : Constr.case_style } + [@@ocaml.deprecated "Alias of Constr.case_printing"] type case_info = Constr.case_info = { ci_ind : Names.inductive; ci_npar : int; ci_cstr_ndecls: int array; ci_cstr_nargs : int array; - ci_pp_info : case_printing + ci_pp_info : Constr.case_printing } + [@@ocaml.deprecated "Alias of Constr.case_info"] type ('constr, 'types) pfixpoint = - (int array * int) * ('constr, 'types) prec_declaration + (int array * int) * ('constr, 'types) Constr.prec_declaration + [@@ocaml.deprecated "Alias of Constr.pfixpoint"] type ('constr, 'types) pcofixpoint = - int * ('constr, 'types) prec_declaration + int * ('constr, 'types) Constr.prec_declaration + [@@ocaml.deprecated "Alias of Constr.pcofixpoint"] type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = | Rel of int | Var of Names.Id.t | Meta of Constr.metavariable - | Evar of 'constr pexistential + | Evar of 'constr Constr.pexistential | Sort of 'sort - | Cast of 'constr * cast_kind * 'types + | Cast of 'constr * 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 @@ -898,50 +1046,77 @@ sig | 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 + | Case of Constr.case_info * 'constr * 'constr * 'constr array + | Fix of ('constr, 'types) Constr.pfixpoint + | CoFix of ('constr, 'types) Constr.pcofixpoint | Proj of Names.Projection.t * 'constr - type existential = Constr.existential_key * 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 + [@@ocaml.deprecated "Alias of Constr.kind_of_term"] + type existential = Evar.t * Constr.constr array + [@@ocaml.deprecated "Alias of Constr.existential"] + type rec_declaration = Names.Name.t array * Constr.constr array * Constr.constr array + [@@ocaml.deprecated "Alias of Constr.rec_declaration"] + val kind_of_term : Constr.constr -> (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) Constr.kind_of_term + [@@ocaml.deprecated "Alias of Constr.kind"] + val applistc : Constr.constr -> Constr.constr list -> Constr.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 + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkVar : Names.Id.t -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkMeta : Constr.metavariable -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] - val mkEvar : existential -> constr + val mkEvar : Constr.existential -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkSort : Sorts.t -> types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkProp : types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkSet : types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkType : Univ.Universe.t -> types - val mkCast : constr * cast_kind * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] + val mkCast : constr * Constr.cast_kind * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkProd : Names.Name.t * types * types -> types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkLambda : Names.Name.t * types * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkLetIn : Names.Name.t * constr * types * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkApp : constr * constr array -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkConst : Names.Constant.t -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkProj : Names.Projection.t * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkInd : Names.inductive -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] 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 + [@@ocaml.deprecated "Alias of similarly named Constr function"] + val mkConstructU : Names.constructor Univ.puniverses -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] + val mkConstructUi : (Constr.pinductive * int) -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] + val mkCase : Constr.case_info * constr * constr * constr array -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkFix : fixpoint -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkCoFix : cofixpoint -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] + 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 + [@@ocaml.deprecated "Alias for the function in [Constr]"] + 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 @@ -953,48 +1128,79 @@ sig val compose_lam : (Names.Name.t * constr) list -> constr -> constr val destSort : constr -> Sorts.t + [@@ocaml.deprecated "Alias for the function in [Constr]"] val destVar : constr -> Names.Id.t + [@@ocaml.deprecated "Alias for the function in [Constr]"] val destApp : constr -> constr * constr array + [@@ocaml.deprecated "Alias for the function in [Constr]"] val destProd : types -> Names.Name.t * types * types + [@@ocaml.deprecated "Alias for the function in [Constr]"] val destLetIn : constr -> Names.Name.t * constr * types * constr - val destEvar : constr -> existential + [@@ocaml.deprecated "Alias for the function in [Constr]"] + val destEvar : constr -> Constr.existential + [@@ocaml.deprecated "Alias for the function in [Constr]"] val destRel : constr -> int - val destConst : constr -> Names.Constant.t puniverses - val destCast : constr -> constr * cast_kind * constr + [@@ocaml.deprecated "Alias for the function in [Constr]"] + val destConst : constr -> Names.Constant.t Univ.puniverses + [@@ocaml.deprecated "Alias for the function in [Constr]"] + val destCast : constr -> constr * Constr.cast_kind * constr + [@@ocaml.deprecated "Alias for the function in [Constr]"] val destLambda : constr -> Names.Name.t * types * constr + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isRel : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isVar : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isEvar : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isLetIn : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isLambda : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isConst : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isEvar_or_Meta : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isCast : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isMeta : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val isApp : constr -> bool + [@@ocaml.deprecated "Alias for the function in [Constr]"] val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a + [@@ocaml.deprecated "Alias of Constr.fold"] val eq_constr : constr -> constr -> bool + [@@ocaml.deprecated "Alias of Constr.equal"] val hash_constr : constr -> int + [@@ocaml.deprecated "Alias of Constr.hash"] + 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 + [@@ocaml.deprecated "Alias of Constr.map"] - val mkIndU : pinductive -> constr - val mkConstU : pconstant -> constr + val mkIndU : Constr.pinductive -> constr + [@@ocaml.deprecated "Alias of Constr.mkIndU"] + val mkConstU : Constr.pconstant -> constr + [@@ocaml.deprecated "Alias of Constr.mkConstU"] val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr + [@@ocaml.deprecated "Alias of Constr.map_with_binders"] + val iter_constr : (constr -> unit) -> constr -> unit + [@@ocaml.deprecated "Alias of Constr.iter."] (* 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 + [@@ocaml.deprecated "Alias of Constr.qe_constr_nounivs."] type ('constr, 'types) kind_of_type = | SortType of Sorts.t @@ -1008,25 +1214,43 @@ sig val is_prop_sort : Sorts.t -> bool [@@ocaml.deprecated "alias of API.Sorts.is_prop"] - type existential_key = Constr.existential_key + type existential_key = Evar.t + [@@ocaml.deprecated "Alias of Constr.existential_key"] val family_of_sort : Sorts.t -> Sorts.family + [@@ocaml.deprecated "Alias of Sorts.family"] val compare : constr -> constr -> int + [@@ocaml.deprecated "Alias of Constr.compare."] val constr_ord : constr -> constr -> int - [@@ocaml.deprecated "alias of API.Term.compare"] + [@@ocaml.deprecated "alias of Term.compare"] - val destInd : constr -> Names.inductive puniverses + val destInd : constr -> Names.inductive Univ.puniverses + [@@ocaml.deprecated "Alias for the function in [Constr]"] val univ_of_sort : Sorts.t -> Univ.Universe.t + [@@ocaml.deprecated "Alias for the function in [Constr]"] val strip_lam : constr -> constr val strip_prod_assum : types -> types val decompose_lam_assum : constr -> Context.Rel.t * constr val destFix : constr -> fixpoint + [@@ocaml.deprecated "Alias for the function in [Constr]"] val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool + [@@ocaml.deprecated "Alias of Constr.compare_head."] + + type constr = Constr.t + [@@ocaml.deprecated "Alias of Constr.t"] + type types = Constr.t + [@@ocaml.deprecated "Alias of Constr.types"] + + type fixpoint = (int array * int) * Constr.rec_declaration + [@@ocaml.deprecated "Alias of Constr.Constr.fixpoint"] + type cofixpoint = int * Constr.rec_declaration + [@@ocaml.deprecated "Alias of Constr.cofixpoint"] + end module Mod_subst : @@ -1078,6 +1302,10 @@ sig | CoFinite | BiFinite + type discharge = + | DoDischarge + | NoDischarge + type locality = | Discharge | Local @@ -1096,6 +1324,7 @@ sig | IdentityCoercion | Instance | Method + | Let type theorem_kind = | Theorem | Lemma @@ -1199,8 +1428,8 @@ sig | TemplateArity of 'b type constant_universes = - | Monomorphic_const of Univ.universe_context - | Polymorphic_const of Univ.abstract_universe_context + | Monomorphic_const of Univ.ContextSet.t + | Polymorphic_const of Univ.AUContext.t type projection_body = { proj_ind : Names.MutInd.t; @@ -1219,7 +1448,7 @@ sig type constant_body = { const_hyps : Context.Named.t; const_body : constant_def; - const_type : Term.types; + const_type : Constr.types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; const_proj : projection_body option; @@ -1266,12 +1495,12 @@ sig | MEwith of module_alg_expr * with_declaration type abstract_inductive_universes = - | Monomorphic_ind of Univ.universe_context - | Polymorphic_ind of Univ.abstract_universe_context - | Cumulative_ind of Univ.abstract_cumulativity_info + | Monomorphic_ind of Univ.ContextSet.t + | Polymorphic_ind of Univ.AUContext.t + | Cumulative_ind of Univ.ACumulativityInfo.t type record_body = (Id.t * Constant.t array * projection_body array) option - + type mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : record_body option; @@ -1333,9 +1562,9 @@ sig | LocalAssumEntry of constr type inductive_universes = - | Monomorphic_ind_entry of Univ.universe_context - | Polymorphic_ind_entry of Univ.universe_context - | Cumulative_ind_entry of Univ.cumulativity_info + | Monomorphic_ind_entry of Univ.ContextSet.t + | Polymorphic_ind_entry of Univ.UContext.t + | Cumulative_ind_entry of Univ.CumulativityInfo.t type one_inductive_entry = { mind_entry_typename : Id.t; @@ -1362,8 +1591,9 @@ sig type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation type constant_universes_entry = - | Monomorphic_const_entry of Univ.universe_context - | Polymorphic_const_entry of Univ.universe_context + | Monomorphic_const_entry of Univ.ContextSet.t + | Polymorphic_const_entry of Univ.UContext.t + type 'a in_constant_universes_entry = 'a * constant_universes_entry type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -1374,7 +1604,7 @@ sig const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } - type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline + type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline type projection_entry = { proj_entry_ind : MutInd.t; @@ -1404,12 +1634,12 @@ sig utj_val : 'types; utj_type : Sorts.t } - type unsafe_type_judgment = Term.types punsafe_type_judgment + type unsafe_type_judgment = Constr.types punsafe_type_judgment 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 push_rec_types : Constr.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 -> named_context_val -> Context.Named.Declaration.t @@ -1449,13 +1679,13 @@ sig | 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 * Constr.t * fconstr * Constr.t array * fconstr Esubst.subs (* predicate and branches are closures *) + | FFix of Constr.fixpoint * fconstr Esubst.subs + | FCoFix of Constr.cofixpoint * fconstr Esubst.subs + | FCaseT of Constr.case_info * Constr.t * fconstr * Constr.t array * fconstr Esubst.subs (* predicate and branches are closures *) | FLambda of int * (Names.Name.t * Constr.t) list * Constr.t * fconstr Esubst.subs | FProd of Names.Name.t * fconstr * fconstr | FLetIn of Names.Name.t * fconstr * fconstr * Constr.t * fconstr Esubst.subs - | FEvar of Term.existential * fconstr Esubst.subs + | FEvar of Constr.existential * fconstr Esubst.subs | FLIFT of int * fconstr | FCLOS of Constr.t * fconstr Esubst.subs | FLOCKED @@ -1491,7 +1721,7 @@ sig val betaiota : RedFlags.reds val betaiotazeta : RedFlags.reds - val create_clos_infos : ?evars:(Term.existential -> Constr.t option) -> RedFlags.reds -> Environ.env -> clos_infos + val create_clos_infos : ?evars:(Constr.existential -> Constr.t option) -> RedFlags.reds -> Environ.env -> clos_infos val whd_val : clos_infos -> fconstr -> Constr.t @@ -1512,13 +1742,13 @@ sig val whd_betaiotazeta : Environ.env -> Constr.t -> Constr.t - val is_arity : Environ.env -> Term.types -> bool + val is_arity : Environ.env -> Constr.types -> bool - val dest_prod : Environ.env -> Term.types -> Context.Rel.t * Term.types + val dest_prod : Environ.env -> Constr.types -> Context.Rel.t * Constr.types type 'a extended_conversion_function = ?l2r:bool -> ?reds:Names.transparent_state -> Environ.env -> - ?evars:((Term.existential->Constr.t option) * UGraph.t) -> + ?evars:((Constr.existential->Constr.t option) * UGraph.t) -> 'a -> 'a -> unit val conv : Constr.t extended_conversion_function end @@ -1527,7 +1757,7 @@ module Type_errors : sig open Names - open Term + open Constr open Environ type 'constr pguard_error = @@ -1559,9 +1789,9 @@ sig | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of identifier * 'constr - | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment - * (sorts_family * sorts_family * arity_error) option + | ReferenceVariables of Id.t * 'constr + | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment + * (Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int @@ -1593,16 +1823,16 @@ 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 + val type_of_inductive : Environ.env -> mind_specif Univ.puniverses -> Constr.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 * Constr.t list + val find_inductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.t list end module Typeops : sig - val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment - val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types + val infer_type : Environ.env -> Constr.types -> Environ.unsafe_type_judgment + val type_of_constant_in : Environ.env -> Constr.pconstant -> Constr.types end module Mod_typing : @@ -1667,12 +1897,13 @@ sig type glob_constraint = glob_level * Univ.constraint_type * glob_level - type case_style = Term.case_style = + type case_style = Constr.case_style = | LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) + [@@ocaml.deprecated "Alias for Constr.case_style."] type 'a cast_type = | CastConv of 'a @@ -1767,12 +1998,15 @@ end module Univops : sig - val universes_of_constr : Term.constr -> Univ.universe_set - val restrict_universe_context : Univ.universe_context_set -> Univ.universe_set -> Univ.universe_context_set + val universes_of_constr : Constr.constr -> Univ.LSet.t + val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t end module Nameops : sig + + open Names + val atompart_of_id : Names.Id.t -> string val pr_id : Names.Id.t -> Pp.t @@ -1781,19 +2015,28 @@ sig val pr_name : Names.Name.t -> Pp.t [@@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.t - module Name : - sig - include module type of struct include Names.Name end + module Name : sig + include module type of struct include Name end + + val map : (Id.t -> Id.t) -> Name.t -> t val get_id : t -> Names.Id.t val fold_right : (Names.Id.t -> 'a -> 'a) -> t -> 'a -> 'a + end + + val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a + [@@ocaml.deprecated "alias of API.Names"] + + val name_app : (Id.t -> Id.t) -> Name.t -> Name.t + [@@ocaml.deprecated "alias of API.Names"] + + val add_suffix : Id.t -> string -> Id.t + val increment_subscript : Id.t -> Id.t + val make_ident : string -> int option -> Id.t + val out_name : Name.t -> Id.t + [@@ocaml.deprecated "alias of API.Names"] + val pr_lab : Label.t -> Pp.t + [@@ocaml.deprecated "alias of API.Names"] end module Libnames : @@ -1832,12 +2075,18 @@ sig 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.t + [@@ocaml.deprecated "Alias for DirPath.print"] val string_of_path : full_path -> string + val basename : full_path -> Names.Id.t type object_name = full_path * Names.KerName.t - type object_prefix = Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t) + type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; + } module Dirset : Set.S with type elt = DirPath.t module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset @@ -1904,7 +2153,7 @@ module Pattern : sig type case_info_pattern = - { cip_style : Misctypes.case_style; + { cip_style : Constr.case_style; cip_ind : Names.inductive option; cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) cip_extensible : bool (** does this match end with _ => _ ? *) } @@ -1925,8 +2174,8 @@ sig | 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 + | PFix of Constr.fixpoint + | PCoFix of Constr.cofixpoint end @@ -1953,7 +2202,7 @@ sig | ImpossibleCase | MatchingVar of matching_var_kind | VarInstance of Names.Id.t - | SubEvar of Constr.existential_key + | SubEvar of Evar.t end module Glob_term : @@ -1977,7 +2226,7 @@ sig | GLambda of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g | GProd of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g | GLetIn of Names.Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g - | GCases of Term.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g + | GCases of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g | GLetTuple of Names.Name.t list * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g | GIf of 'a glob_constr_g * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g | GRec of 'a fix_kind_g * Names.Id.t array * 'a glob_decl_g list array * @@ -2040,7 +2289,7 @@ sig | 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 * + | NCases of Constr.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) * @@ -2112,7 +2361,7 @@ sig | CApp of (proj_flag * constr_expr) * (constr_expr * explicitation Loc.located option) list | CRecord of (Libnames.reference * constr_expr) list - | CCases of Term.case_style + | CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list @@ -2504,9 +2753,9 @@ module Universes : sig type universe_binders type 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 type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set + val fresh_inductive_instance : Environ.env -> Names.inductive -> Constr.pinductive Univ.in_universe_context_set + val new_Type : Names.DirPath.t -> Constr.types + val type_of_global : Globnames.global_reference -> Constr.types Univ.in_universe_context_set val constr_of_global : Globnames.global_reference -> Constr.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val new_sort_in_family : Sorts.family -> Sorts.t @@ -2530,6 +2779,9 @@ sig val context_set : t -> Univ.ContextSet.t val of_context_set : Univ.ContextSet.t -> t + val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry + val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes + type rigid = | UnivRigid | UnivFlexible of bool @@ -2539,9 +2791,12 @@ end module Evd : sig - type evar = Constr.existential_key + type evar = Evar.t + [@@ocaml.deprecated "use Evar.t"] val string_of_existential : Evar.t -> string + [@@ocaml.deprecated "use Evar.print"] + type evar_constraint = Reduction.conv_pb * Environ.env * Constr.t * Constr.t (* --------------------------------- *) @@ -2618,7 +2873,7 @@ sig val empty : evar_map val from_env : Environ.env -> evar_map val find : evar_map -> Evar.t -> evar_info - val find_undefined : evar_map -> evar -> evar_info + val find_undefined : evar_map -> Evar.t -> 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 @@ -2631,28 +2886,31 @@ sig val create_evar_defs : evar_map -> evar_map - val meta_declare : Constr.metavariable -> Term.types -> ?name:Names.Name.t -> evar_map -> evar_map + val meta_declare : Constr.metavariable -> Constr.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 new_sort_variable : ?loc:Loc.t -> ?name:Names.Id.t -> 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 -> Globnames.global_reference -> evar_map * Constr.t 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 fresh_inductive_instance : ?loc:Loc.t -> Environ.env -> evar_map -> Names.inductive -> evar_map * Constr.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 : evar -> evar_map -> Names.Id.t option + val evar_ident : Evar.t -> 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 -> extensible:bool -> evar_map -> - (Names.Id.t * Univ.Level.t) list * Univ.UContext.t + val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map + val to_universe_context : evar_map -> Univ.UContext.t + val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry + val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes + val meta_list : evar_map -> (Constr.metavariable * clbinding) list val meta_defined : evar_map -> Constr.metavariable -> bool @@ -2699,8 +2957,8 @@ sig type evar_universe_context = UState.t [@@ocaml.deprecated "alias of API.UState.t"] - val existential_opt_value : evar_map -> Term.existential -> Constr.t option - val existential_value : evar_map -> Term.existential -> Constr.t + val existential_opt_value : evar_map -> Constr.existential -> Constr.t option + val existential_value : evar_map -> Constr.existential -> Constr.t exception NotInstantiatedEvar @@ -2931,7 +3189,7 @@ sig val map_constr_with_binders_left_to_right : Evd.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. *) + (** Remove the outer-most {!Constr.kind_of_term.Cast} from a given term. *) val strip_outer_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr (** [nb_lam] ⟦[fun (x1:t1)...(xn:tn) => c]⟧ where [c] is not an abstraction gives [n]. @@ -2942,7 +3200,7 @@ sig 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 + val push_rels_assum : (Names.Name.t * Constr.types) list -> Environ.env -> Environ.env type meta_value_map = (Constr.metavariable * Constr.t) list @@ -3034,6 +3292,7 @@ sig exception ClearDependencyError of Names.Id.t * clear_dependency_error val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t + val has_undefined_evars : Evd.evar_map -> EConstr.constr -> bool 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 -> @@ -3044,7 +3303,7 @@ sig ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> Evd.rigid -> Evd.evar_map * (EConstr.constr * Sorts.t) val nf_evars_universes : Evd.evar_map -> Constr.t -> Constr.t - val safe_evar_value : Evd.evar_map -> Term.existential -> Constr.t option + val safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.t option val evd_comb1 : (Evd.evar_map -> 'b -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'b -> 'a end @@ -3078,7 +3337,7 @@ sig val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t val read_line : string t end - val proofview : proofview -> Evd.evar list * Evd.evar_map + val proofview : proofview -> Evar.t list * Evd.evar_map val cycle : int -> unit tactic val swap : int -> int -> unit tactic val revgoals : unit tactic @@ -3105,20 +3364,20 @@ sig val shelve_unifiable : unit tactic val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview - * (bool * Evd.evar list * Evd.evar list) + * (bool * Evar.t list * Evar.t list) * Proofview_monad.Info.tree val numgoals : int tactic - val with_shelf : 'a tactic -> (Evd.evar list * 'a) tactic + val with_shelf : 'a tactic -> (Evar.t list * 'a) tactic module Unsafe : sig val tclEVARS : Evd.evar_map -> unit tactic - val tclGETGOALS : Evd.evar list tactic + val tclGETGOALS : Evar.t list tactic - val tclSETGOALS : Evd.evar list -> unit tactic + val tclSETGOALS : Evar.t list -> unit tactic - val tclNEWGOALS : Evd.evar list -> unit tactic + val tclNEWGOALS : Evar.t list -> unit tactic end module Goal : @@ -3412,14 +3671,14 @@ sig | IndType of inductive_family * EConstr.constr list type constructor_summary = { - cs_cstr : Term.pconstructor; + cs_cstr : Constr.pconstructor; cs_params : Constr.t list; cs_nargs : int; cs_args : Context.Rel.t; cs_concl_realargs : Constr.t array; } - val arities_of_constructors : Environ.env -> Term.pinductive -> Term.types array + val arities_of_constructors : Environ.env -> Constr.pinductive -> Constr.types array val constructors_nrealargs_env : Environ.env -> Names.inductive -> int array val constructor_nallargs_env : Environ.env -> Names.constructor -> int @@ -3427,16 +3686,16 @@ sig val inductive_nparamdecls : Names.inductive -> int - val type_of_constructors : Environ.env -> Term.pinductive -> Term.types array + val type_of_constructors : Environ.env -> Constr.pinductive -> Constr.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 * Constr.t list + val dest_ind_family : inductive_family -> Names.inductive Univ.puniverses * Constr.t list val find_inductive : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * Constr.t list - val type_of_inductive : Environ.env -> Term.pinductive -> Term.types + val type_of_inductive : Environ.env -> Constr.pinductive -> Constr.types end module Impargs : @@ -3462,7 +3721,7 @@ 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 get_sort_family_of : ?truncation_style:bool -> ?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 @@ -3778,8 +4037,6 @@ sig type verbose_flag = bool - type obsolete_locality = bool - type universe_decl_expr = (lident list, Misctypes.glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option @@ -3894,29 +4151,27 @@ sig | VernacRedirect of string * vernac_expr Loc.located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr - | VernacSyntaxExtension of - bool * obsolete_locality * (lstring * syntax_modifier list) - | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) + | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) + | VernacOpenCloseScope of bool * scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list - | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * + | VernacInfix of (lstring * syntax_modifier list) * Constrexpr.constr_expr * scope_name option | VernacNotation of - obsolete_locality * Constrexpr.constr_expr * (lstring * syntax_modifier list) * + 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) * ident_decl * definition_expr + | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * ident_decl * definition_expr | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of Constrexpr.constr_expr - | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * + | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * inline * (ident_decl list * Constrexpr.constr_expr) with_coercion list | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of - Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list + Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of - Decl_kinds.locality option * (cofixpoint_expr * decl_notation list) list + Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -3927,9 +4182,9 @@ sig Libnames.reference option * bool option * Libnames.reference list | VernacImport of bool * Libnames.reference list | VernacCanonical of Libnames.reference Misctypes.or_by_notation - | VernacCoercion of obsolete_locality * Libnames.reference Misctypes.or_by_notation * + | VernacCoercion of Libnames.reference Misctypes.or_by_notation * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of obsolete_locality * lident * + | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr | VernacNameSectionHypSet of lident * section_subset_expr | VernacInstance of @@ -3963,9 +4218,9 @@ sig | VernacBackTo of int | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * Libnames.reference list - | VernacHints of obsolete_locality * string list * hints_expr + | VernacHints of string list * hints_expr | VernacSyntacticDefinition of Names.Id.t Loc.located * (Names.Id.t list * Constrexpr.constr_expr) * - obsolete_locality * onlyparsing_flag + onlyparsing_flag | VernacDeclareImplicits of Libnames.reference Misctypes.or_by_notation * (Constrexpr.explicitation * bool * bool) list list | VernacArguments of Libnames.reference Misctypes.or_by_notation * @@ -4088,12 +4343,12 @@ 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 -> + val build_case_analysis_scheme : Environ.env -> Evd.evar_map -> Constr.pinductive -> dep_flag -> Sorts.family -> Evd.evar_map * Constr.t 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 * Constr.t list - val build_case_analysis_scheme_default : Environ.env -> Evd.evar_map -> Term.pinductive -> + Environ.env -> Evd.evar_map -> (Constr.pinductive * dep_flag * Sorts.family) list -> Evd.evar_map * Constr.t list + val build_case_analysis_scheme_default : Environ.env -> Evd.evar_map -> Constr.pinductive -> Sorts.family -> Evd.evar_map * Constr.t end @@ -4287,6 +4542,8 @@ sig 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 + val replace_vars_constr_expr : + Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr end module Notation_ops : @@ -4341,8 +4598,11 @@ end module Topconstr : sig + val replace_vars_constr_expr : - Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr + Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr + [@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] + end module Constrintern : @@ -4383,13 +4643,13 @@ sig 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 + Constrexpr.constr_expr -> Constr.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 + Constr.types -> Impargs.manual_explicitation list -> var_internalization_data val empty_internalization_env : internalization_env val global_reference : Names.Id.t -> Globnames.global_reference end @@ -4418,7 +4678,7 @@ sig type 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 + | SectionLocalAssum of Constr.types Univ.in_universe_context_set * Decl_kinds.polymorphic * bool type variable_declaration = Names.DirPath.t * section_variable_entry * Decl_kinds.logical_kind @@ -4429,11 +4689,11 @@ sig val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind -> - ?local:bool -> ?poly:Decl_kinds.polymorphic -> Names.Id.t -> ?types:Constr.t -> - Constr.t Univ.in_universe_context_set -> Names.Constant.t + ?local:bool -> Names.Id.t -> ?types:Constr.t -> + Constr.t Entries.in_constant_universes_entry -> 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 -> + ?opaque:bool -> ?inline:bool -> ?types:Constr.types -> + ?univs:Entries.constant_universes_entry -> ?eff:Safe_typing.private_constants -> Constr.t -> 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 @@ -4540,19 +4800,28 @@ end module Proof : sig - type proof + type t + type proof = t + [@@ocaml.deprecated "please use [Proof.t]"] + type 'a focus_kind + val proof : t -> + Goal.goal list * (Goal.goal list * Goal.goal list) list * + Goal.goal list * Goal.goal list * Evd.evar_map 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.t + unit Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree) + val unshelve : t -> t + val maximal_unfocus : 'a focus_kind -> t -> t + val pr_proof : t -> Pp.t + module V82 : sig - val grab_evars : proof -> proof + val grab_evars : t -> t + + val subgoals : t -> Goal.goal list Evd.sigma + [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] - val subgoals : proof -> Goal.goal list Evd.sigma end end @@ -4564,7 +4833,9 @@ end module Proof_global : sig - type state + type t + type state = t + [@@ocaml.deprecated "please use [Proof_global.t]"] type proof_mode = { name : string; @@ -4595,14 +4866,14 @@ sig Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit val with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof * 'a) -> 'a + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a val simple_with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit + (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit val compact_the_proof : unit -> unit val register_proof_mode : proof_mode -> unit exception NoCurrentProof - val give_me_the_proof : unit -> Proof.proof + val give_me_the_proof : unit -> Proof.t (** @raise NoCurrentProof when outside proof mode. *) val discard_all : unit -> unit @@ -4733,7 +5004,7 @@ sig 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 + Proof.t -> Proof.t * bool val cook_proof : unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind)) @@ -4839,7 +5110,6 @@ sig val ident : Id.t Gram.entry val name : Name.t located Gram.entry val identref : Id.t located Gram.entry - val pidentref : (Id.t located * (Id.t located list) option) Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : Id.t located Gram.entry val base_ident : Id.t Gram.entry @@ -5036,12 +5306,20 @@ sig val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t val pr_constr : Constr.t -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr : Constr.t -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr : EConstr.constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_glob_constr : Glob_term.glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_constr_pattern : Pattern.constr_pattern -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t @@ -5049,11 +5327,17 @@ sig val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lglob_constr : Glob_term.glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_leconstr : EConstr.constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_global : Globnames.global_reference -> Pp.t val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t @@ -5061,8 +5345,11 @@ sig val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t - val pr_ltype : Term.types -> Pp.t + val pr_ltype : Constr.types -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_idpred : Names.Id.Pred.t -> Pp.t val pr_cpred : Names.Cpred.t -> Pp.t val pr_transparent_state : Names.transparent_state -> Pp.t @@ -5491,7 +5778,7 @@ end module Hints : sig - type raw_hint = EConstr.t * EConstr.types * Univ.universe_context_set + type raw_hint = EConstr.t * EConstr.types * Univ.ContextSet.t type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) @@ -5575,7 +5862,9 @@ sig 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_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t + [@@ocaml.deprecated "please used pr_hint_db_env"] end module Auto : @@ -5639,7 +5928,7 @@ end module Autorewrite : sig type rew_rule = { rew_lemma: Constr.t; - rew_type: Term.types; + rew_type: Constr.types; rew_pat: Constr.t; rew_ctx: Univ.ContextSet.t; rew_l2r: bool; @@ -5652,7 +5941,7 @@ sig val add_rew_rules : string -> raw_rew_rule list -> unit val find_rewrites : string -> rew_rule list val find_matches : string -> Constr.t -> rew_rule list - val print_rewrite_hintdb : string -> Pp.t + val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t end (************************************************************************) @@ -5685,11 +5974,12 @@ sig 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 + [@@ocaml.deprecated "please use [Pfedit.get_current_context]"] end module Himsg : sig - val explain_refiner_error : Logic.refiner_error -> Pp.t + val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t end @@ -5702,9 +5992,6 @@ 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 @@ -5827,14 +6114,37 @@ sig Names.Id.t end +module Vernacstate : +sig + + type t = { + system : States.state; (* summary + libstack *) + proof : Proof_global.t; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) + } + + (* XXX: This should not be exported *) + val freeze_interp_state : Summary.marshallable -> t + val unfreeze_interp_state : t -> unit + +end + module Vernacinterp : sig + type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit + type atts = { + loc : Loc.t option; + locality : bool option; + polymorphic : bool; + } + + type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t - val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit + type plugin_args = Genarg.raw_generic_argument list + + val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit end @@ -5856,15 +6166,6 @@ end module Vernacentries : sig - type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) - } - - val freeze_interp_state : Summary.marshallable -> interp_state - val unfreeze_interp_state : interp_state -> unit - val dump_global : Libnames.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 @@ -5896,7 +6197,7 @@ sig val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] end (************************************************************************) |