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 /library/global.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 'library/global.mli')
| -rw-r--r-- | library/global.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/global.mli b/library/global.mli index 388fee527..f7306fe57 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,9 +32,9 @@ val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : - chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit + flags:Declarations.typing_flags -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit val push_named_def : - chkguard:bool -> (Id.t * Entries.definition_entry) -> unit + flags:Declarations.typing_flags -> (Id.t * Entries.definition_entry) -> unit val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant |