From 53ced0735f7e24735d78a02fc74588b8d9186eab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 Jun 2016 18:25:02 +0200 Subject: Moving the typing_flags to the environment. --- kernel/safe_typing.mli | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b614a368c..15ebc7d88 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -77,21 +77,19 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - flags:Declarations.typing_flags -> (Id.t * Term.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 : - flags:Declarations.typing_flags -> Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) type global_declaration = (* bool: export private constants *) - | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe type exported_private_constant = @@ -134,6 +132,7 @@ val add_constraints : (** Setting the type theory flavor *) val set_engagement : Declarations.engagement -> safe_transformer0 +val set_typing_flags : Declarations.typing_flags -> safe_transformer0 (** {6 Interactive module functions } *) -- cgit v1.2.3