diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 300 |
1 files changed, 165 insertions, 135 deletions
diff --git a/API/API.mli b/API/API.mli index 2aa5da67da..abbdf22b91 100644 --- a/API/API.mli +++ b/API/API.mli @@ -491,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 @@ -516,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 @@ -594,7 +600,7 @@ sig 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 @@ -605,7 +611,7 @@ sig 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 @@ -695,16 +701,16 @@ sig val decompose_appvect : constr -> constr * constr array (** Destructs a constant *) - val destConst : constr -> Constant.t puniverses + val destConst : constr -> Constant.t Univ.puniverses (** Destructs an existential variable *) val destEvar : constr -> existential (** Destructs a (co)inductive type *) - val destInd : constr -> inductive puniverses + val destInd : constr -> inductive Univ.puniverses (** Destructs a constructor *) - val destConstruct : constr -> constructor puniverses + 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 @@ -988,11 +994,11 @@ sig type 'a puniverses = 'a Univ.puniverses [@@ocaml.deprecated "Alias of Constr.puniverses"] - type pconstant = Names.Constant.t Constr.puniverses + type pconstant = Names.Constant.t Univ.puniverses [@@ocaml.deprecated "Alias of Constr.pconstant"] - type pinductive = Names.inductive Constr.puniverses + type pinductive = Names.inductive Univ.puniverses [@@ocaml.deprecated "Alias of Constr.pinductive"] - type pconstructor = Names.constructor Constr.puniverses + type pconstructor = Names.constructor Univ.puniverses [@@ocaml.deprecated "Alias of Constr.pconstructor"] type case_style = Constr.case_style = | LetStyle @@ -1045,7 +1051,7 @@ sig | CoFix of ('constr, 'types) Constr.pcofixpoint | Proj of Names.Projection.t * 'constr [@@ocaml.deprecated "Alias of Constr.kind_of_term"] - type existential = Constr.existential_key * Constr.constr array + 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"] @@ -1093,7 +1099,7 @@ sig [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkConstruct : Names.constructor -> constr [@@ocaml.deprecated "Alias of similarly named Constr function"] - val mkConstructU : Names.constructor Constr.puniverses -> constr + 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"] @@ -1135,7 +1141,7 @@ sig [@@ocaml.deprecated "Alias for the function in [Constr]"] val destRel : constr -> int [@@ocaml.deprecated "Alias for the function in [Constr]"] - val destConst : constr -> Names.Constant.t Constr.puniverses + 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]"] @@ -1208,7 +1214,7 @@ 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 @@ -1220,7 +1226,7 @@ sig val constr_ord : constr -> constr -> int [@@ocaml.deprecated "alias of Term.compare"] - val destInd : constr -> Names.inductive Constr.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]"] @@ -1296,6 +1302,10 @@ sig | CoFinite | BiFinite + type discharge = + | DoDischarge + | NoDischarge + type locality = | Discharge | Local @@ -1314,6 +1324,7 @@ sig | IdentityCoercion | Instance | Method + | Let type theorem_kind = | Theorem | Lemma @@ -1417,7 +1428,7 @@ sig | TemplateArity of 'b type constant_universes = - | Monomorphic_const of Univ.UContext.t + | Monomorphic_const of Univ.ContextSet.t | Polymorphic_const of Univ.AUContext.t type projection_body = { @@ -1484,7 +1495,7 @@ sig | MEwith of module_alg_expr * with_declaration type abstract_inductive_universes = - | Monomorphic_ind of Univ.UContext.t + | Monomorphic_ind of Univ.ContextSet.t | Polymorphic_ind of Univ.AUContext.t | Cumulative_ind of Univ.ACumulativityInfo.t @@ -1551,7 +1562,7 @@ sig | LocalAssumEntry of constr type inductive_universes = - | Monomorphic_ind_entry of Univ.UContext.t + | Monomorphic_ind_entry of Univ.ContextSet.t | Polymorphic_ind_entry of Univ.UContext.t | Cumulative_ind_entry of Univ.CumulativityInfo.t @@ -1580,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.UContext.t + | 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 *) @@ -1592,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; @@ -1849,6 +1861,60 @@ end (* Modules from intf/ *) (************************************************************************) +module Libnames : +sig + + open Util + open Names + + type full_path + val pr_path : full_path -> Pp.t + val make_path : Names.DirPath.t -> Names.Id.t -> full_path + val eq_full_path : full_path -> full_path -> bool + val repr_path : full_path -> Names.DirPath.t * Names.Id.t + val dirpath : full_path -> Names.DirPath.t + val path_of_string : string -> full_path + + type 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.t + 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 = + | Qualid of 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.t + + 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.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 = { + 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 + module Spmap : CSig.MapS with type key = full_path +end + module Misctypes : sig type evars_flag = bool @@ -1871,10 +1937,15 @@ sig | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) - type level_info = Names.Name.t Loc.located option + type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + + type level_info = Libnames.reference universe_kind type glob_level = level_info glob_sort_gen - type sort_info = Names.Name.t Loc.located list + type sort_info = (Libnames.reference * int) option list type glob_sort = sort_info glob_sort_gen type ('a, 'b) gen_universe_decl = { @@ -2027,56 +2098,6 @@ sig [@@ocaml.deprecated "alias of API.Names"] end -module Libnames : -sig - - open Util - open Names - - type full_path - val pr_path : full_path -> Pp.t - val make_path : Names.DirPath.t -> Names.Id.t -> full_path - val eq_full_path : full_path -> full_path -> bool - val repr_path : full_path -> Names.DirPath.t * Names.Id.t - val dirpath : full_path -> Names.DirPath.t - val path_of_string : string -> full_path - - type 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.t - 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 = - | Qualid of 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.t - - 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.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) - - module Dirset : Set.S with type elt = DirPath.t - module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset - module Spmap : CSig.MapS with type key = full_path -end - module Globnames : sig @@ -2186,7 +2207,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 : @@ -2738,10 +2759,10 @@ sig type universe_binders type universe_opt_subst val fresh_inductive_instance : Environ.env -> Names.inductive -> Constr.pinductive Univ.in_universe_context_set - val new_Type : Names.DirPath.t -> Constr.types + val new_Type : unit -> 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_univ_level : unit -> Univ.Level.t val new_sort_in_family : Sorts.family -> Sorts.t val pr_with_global_universes : Univ.Level.t -> Pp.t val pr_universe_opt_subst : universe_opt_subst -> Pp.t @@ -2763,6 +2784,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 @@ -2772,9 +2796,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 (* --------------------------------- *) @@ -2851,7 +2878,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 @@ -2869,7 +2896,7 @@ sig 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 -> @@ -2879,13 +2906,16 @@ sig 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 @@ -3267,6 +3297,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 -> @@ -3311,7 +3342,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 @@ -3338,20 +3369,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 : @@ -3667,7 +3698,7 @@ sig 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 Constr.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 -> Constr.pinductive -> Constr.types end @@ -3695,7 +3726,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 @@ -4011,8 +4042,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 @@ -4127,29 +4156,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 @@ -4160,9 +4187,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 @@ -4196,9 +4223,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 * @@ -4667,11 +4694,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:Constr.types -> - ?poly:Decl_kinds.polymorphic -> ?univs:Univ.UContext.t -> + ?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 @@ -4778,24 +4805,26 @@ end module Proof : sig - type proof - type 'a focus_kind + type t + type proof = t + [@@ocaml.deprecated "please use [Proof.t]"] - val proof : proof -> + 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 : proof -> Goal.goal list Evd.sigma + val subgoals : t -> Goal.goal list Evd.sigma [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] end @@ -4809,24 +4838,25 @@ end module Proof_global : sig - type state + type t + type state = t + [@@ocaml.deprecated "please use [Proof_global.t]"] type proof_mode = { name : string; set : unit -> unit ; reset : unit -> unit } - type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - proof_universes + UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -4840,14 +4870,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 @@ -4978,9 +5008,9 @@ 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)) + unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind)) val get_current_context : unit -> Evd.evar_map * Environ.env val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types @@ -6095,9 +6125,9 @@ end module Vernacstate : sig - type t = { (* TODO: inline records in OCaml 4.03 *) + type t = { system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) + proof : Proof_global.t; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } @@ -6115,14 +6145,14 @@ sig type atts = { loc : Loc.t option; locality : bool option; + polymorphic : bool; } - type vernac_command = - Genarg.raw_generic_argument list -> - atts:atts -> st:Vernacstate.t -> - Vernacstate.t + type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t + + type plugin_args = Genarg.raw_generic_argument list - val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit + val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit end |