diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a57fb108c..80b9bb495 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,14 +57,16 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : + chkguard:bool -> (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 val push_named_def : + chkguard:bool -> Id.t * Entries.definition_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry + | ConstantEntry of Entries.constant_entry * bool (* chkguard *) | GlobalRecipe of Cooking.recipe val add_constant : |