diff options
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 |