diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2016-06-07 09:52:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2016-06-14 20:01:37 +0200 |
| commit | d4f3a1a807d474050a4e91e16ff7813f1db7f537 (patch) | |
| tree | 68c91e818fd7d35789c514b3db06f77ed54b8968 /kernel/safe_typing.mli | |
| parent | 64e94267cb80adc1b4df782cc83a579ee521b59b (diff) | |
Assume totality: dedicated type rather than bool
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 80b9bb495..c5e43e42a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,16 +57,16 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - chkguard:bool -> + flags:Declarations.typing_flags -> (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 val push_named_def : - chkguard:bool -> + flags:Declarations.typing_flags -> Id.t * Entries.definition_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry * bool (* chkguard *) + | ConstantEntry of Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe val add_constant : |