diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 69 |
1 files changed, 31 insertions, 38 deletions
diff --git a/library/global.mli b/library/global.mli index 15bf58f82..324181e79 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,44 +32,44 @@ val set_typing_flags : Declarations.typing_flags -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set +val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.ContextSet.t val export_private_constants : in_section:bool -> Safe_typing.private_constants Entries.constant_entry -> unit Entries.constant_entry * Safe_typing.exported_private_constant list val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant + DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t val add_mind : - DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive + DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t (** Extra universe constraints *) -val add_constraints : Univ.constraints -> unit +val add_constraints : Univ.Constraint.t -> unit -val push_context : bool -> Univ.universe_context -> unit -val push_context_set : bool -> Univ.universe_context_set -> unit +val push_context : bool -> Univ.UContext.t -> unit +val push_context_set : bool -> Univ.ContextSet.t -> unit (** Non-interactive modules and module types *) val add_module : Id.t -> Entries.module_entry -> Declarations.inline -> - module_path * Mod_subst.delta_resolver + ModPath.t * Mod_subst.delta_resolver val add_modtype : - Id.t -> Entries.module_type_entry -> Declarations.inline -> module_path + Id.t -> Entries.module_type_entry -> Declarations.inline -> ModPath.t val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver (** Interactive modules and module types *) -val start_module : Id.t -> module_path -val start_modtype : Id.t -> module_path +val start_module : Id.t -> ModPath.t +val start_modtype : Id.t -> ModPath.t val end_module : Summary.frozen -> Id.t -> (Entries.module_struct_entry * Declarations.inline) option -> - module_path * MBId.t list * Mod_subst.delta_resolver + ModPath.t * MBId.t list * Mod_subst.delta_resolver -val end_modtype : Summary.frozen -> Id.t -> module_path * MBId.t list +val end_modtype : Summary.frozen -> Id.t -> ModPath.t * MBId.t list val add_module_parameter : MBId.t -> Entries.module_struct_entry -> Declarations.inline -> @@ -78,45 +78,38 @@ val add_module_parameter : (** {6 Queries in the global environment } *) val lookup_named : variable -> Context.Named.Declaration.t -val lookup_constant : constant -> Declarations.constant_body +val lookup_constant : Constant.t -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_pinductive : Constr.pinductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body -val lookup_mind : mutual_inductive -> Declarations.mutual_inductive_body -val lookup_module : module_path -> Declarations.module_body -val lookup_modtype : module_path -> Declarations.module_type_body +val lookup_mind : MutInd.t -> Declarations.mutual_inductive_body +val lookup_module : ModPath.t -> Declarations.module_body +val lookup_modtype : ModPath.t -> Declarations.module_type_body val exists_objlabel : Label.t -> bool -val constant_of_delta_kn : kernel_name -> constant -val mind_of_delta_kn : kernel_name -> mutual_inductive +val constant_of_delta_kn : KerName.t -> Constant.t +val mind_of_delta_kn : KerName.t -> MutInd.t val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option +val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option (** Returns the body of the constant if it has any, and the polymorphic context it lives in. For monomorphic constant, the latter is empty, and for polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated. *) -val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option +val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) -(** Global universe name <-> level mapping *) -type universe_names = - (Decl_kinds.polymorphic * Univ.universe_level) Id.Map.t * Id.t Univ.LMap.t - -val global_universe_names : unit -> universe_names -val set_global_universe_names : universe_names -> unit - (** {6 Compiled libraries } *) -val start_library : DirPath.t -> module_path +val start_library : DirPath.t -> ModPath.t val export : ?except:Future.UUIDSet.t -> DirPath.t -> - module_path * Safe_typing.compiled_library * Safe_typing.native_library + ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library val import : - Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest -> - module_path + Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest -> + ModPath.t (** {6 Misc } *) @@ -147,23 +140,23 @@ val type_of_global_in_context : Environ.env -> constants, it does not matter. *) (** Returns the universe context of the global reference (whatever its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context +val universes_of_global : Globnames.global_reference -> Univ.AUContext.t (** {6 Retroknowledge } *) val register : - Retroknowledge.field -> Term.constr -> Term.constr -> unit + Retroknowledge.field -> Constr.constr -> Constr.constr -> unit -val register_inline : constant -> unit +val register_inline : Constant.t -> unit (** {6 Oracle } *) -val set_strategy : Names.constant Names.tableKey -> Conv_oracle.level -> unit +val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit (* Modifies the global state, registering new universes *) -val current_dirpath : unit -> Names.dir_path +val current_dirpath : unit -> DirPath.t -val with_global : (Environ.env -> Names.dir_path -> 'a Univ.in_universe_context_set) -> 'a +val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a -val global_env_summary_name : string +val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag |