diff options
| author | Gaëtan Gilbert | 2019-07-02 12:35:49 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 17:01:29 +0200 |
| commit | d324c858be652659a5062332f00e7d20393a48be (patch) | |
| tree | 8e36d767d1a11e47e9c825c3a8e96fd0f7fddf87 /library | |
| parent | 5a6de0ece2436a0fe49750ba0ec26da90f0417e3 (diff) | |
Safe_typing.push_named_assum: don't take universes
The caller should push them first
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli index 51307b3604..d034bc4208 100644 --- a/library/global.mli +++ b/library/global.mli @@ -38,7 +38,7 @@ val sprop_allowed : unit -> bool (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit +val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit val export_private_constants : in_section:bool -> |