From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- kernel/safe_typing.mli | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index ee9632944..0bfe07486 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -69,7 +69,7 @@ val inline_private_constants_in_constr : val inline_private_constants_in_definition_entry : Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry -val universes_of_private : private_constants -> Univ.universe_context_set list +val universes_of_private : private_constants -> Univ.ContextSet.t list val is_curmod_library : safe_environment -> bool @@ -84,13 +84,13 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - (Id.t * Term.types * bool (* polymorphic *)) + (Id.t * Constr.types * bool (* polymorphic *)) Univ.in_universe_context_set -> safe_transformer0 (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer + Id.t * private_constants Entries.definition_entry -> Univ.ContextSet.t safe_transformer (** Insertion of global axioms or definitions *) @@ -133,10 +133,10 @@ val add_modtype : (** Adding universe constraints *) val push_context_set : - bool -> Univ.universe_context_set -> safe_transformer0 + bool -> Univ.ContextSet.t -> safe_transformer0 val push_context : - bool -> Univ.universe_context -> safe_transformer0 + bool -> Univ.UContext.t -> safe_transformer0 val add_constraints : Univ.constraints -> safe_transformer0 @@ -194,18 +194,18 @@ val export : ModPath.t * compiled_library * native_library (* Constraints are non empty iff the file is a vi2vo *) -val import : compiled_library -> Univ.universe_context_set -> vodigest -> +val import : compiled_library -> Univ.ContextSet.t -> vodigest -> ModPath.t safe_transformer (** {6 Safe typing judgments } *) type judgment -val j_val : judgment -> Term.constr -val j_type : judgment -> Term.constr +val j_val : judgment -> Constr.constr +val j_type : judgment -> Constr.constr (** The safe typing of a term returns a typing judgment. *) -val typing : safe_environment -> Term.constr -> judgment +val typing : safe_environment -> Constr.constr -> judgment (** {6 Queries } *) @@ -221,7 +221,7 @@ open Retroknowledge val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a val register : - field -> Retroknowledge.entry -> Term.constr -> safe_transformer0 + field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 val register_inline : Constant.t -> safe_transformer0 -- cgit v1.2.3