diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-17 18:25:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-18 18:54:43 +0200 |
| commit | 53ced0735f7e24735d78a02fc74588b8d9186eab (patch) | |
| tree | 93661920f42d9be934e59f5f972d165ea24785b7 /kernel/safe_typing.mli | |
| parent | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (diff) | |
Moving the typing_flags to the environment.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 5 |
1 files changed, 2 insertions, 3 deletions
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 } *) |