diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-07-24 08:46:09 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 10:41:41 +0200 |
| commit | e8bad8abc7be351a34fdf9770409bbab14bcd6a9 (patch) | |
| tree | 00ca0103024f39e5943dcce5a89e9283708ae323 /library/global.mli | |
| parent | 8f64e84a3560bcf668b00ac93ab33542456a9bda (diff) | |
Propagate `Guarded` flag from syntax to kernel.
The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/library/global.mli b/library/global.mli index 248e1f86d..388fee527 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,8 +31,10 @@ val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> unit +val push_named_assum : + chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit +val push_named_def : + chkguard:bool -> (Id.t * Entries.definition_entry) -> unit val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant |