diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 30 |
1 files changed, 19 insertions, 11 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index d70d7d8be..ad2148ead 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -55,9 +55,9 @@ val join_safe_environment : safe_environment -> safe_environment (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - Id.t * Term.types -> Univ.constraints safe_transformer + (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 val push_named_def : - Id.t * Entries.definition_entry -> Univ.constraints safe_transformer + Id.t * Entries.definition_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) @@ -85,10 +85,19 @@ val add_modtype : (** Adding universe constraints *) -val add_constraints : Univ.constraints -> safe_transformer0 +val push_context_set : + Univ.universe_context_set -> safe_transformer0 -(** Setting the Set-impredicative engagement *) +val push_context : + Univ.universe_context -> safe_transformer0 +val add_constraints : + Univ.constraints -> safe_transformer0 + +(* (\** Generator of universes *\) *) +(* val next_universe : int safe_transformer *) + +(** Settin the strongly constructive or classical logical engagement *) val set_engagement : Declarations.engagement -> safe_transformer0 (** {6 Interactive module functions } *) @@ -113,6 +122,10 @@ val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer +val current_modpath : safe_environment -> module_path + +val current_dirpath : safe_environment -> dir_path + (** {6 Libraries : loading and saving compilation units } *) type compiled_library @@ -137,12 +150,7 @@ type judgment val j_val : judgment -> Term.constr val j_type : judgment -> Term.constr -(** The safe typing of a term returns a typing judgment and some universe - constraints (to be added to the environment for the judgment to - hold). It is guaranteed that the constraints are satisfiable. - *) -val safe_infer : safe_environment -> Term.constr -> judgment * Univ.constraints - +(** The safe typing of a term returns a typing judgment. *) val typing : safe_environment -> Term.constr -> judgment (** {6 Queries } *) @@ -164,4 +172,4 @@ val register : val register_inline : constant -> safe_transformer0 val set_strategy : - safe_environment -> 'a Names.tableKey -> Conv_oracle.level -> safe_environment + safe_environment -> Names.constant Names.tableKey -> Conv_oracle.level -> safe_environment |