diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-01 18:42:38 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:13 +0200 |
| commit | 4585baa53e7fa4c25e304b8136944748a7622e10 (patch) | |
| tree | b8a6b71eff51d1f1ef8367bdf420754597dcd8c3 /library/global.ml | |
| parent | de648c72a79ae5ba35db166575669ca465b11770 (diff) | |
Univs: refined handling of assumptions
According to their polymorphic/non-polymorphic status, which
imply that universe variables introduced with it are assumed
to be >= or > Set respectively in the following definitions.
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/global.ml b/library/global.ml index 0419799b6..382abb846 100644 --- a/library/global.ml +++ b/library/global.ml @@ -80,8 +80,8 @@ let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) -let push_context_set c = globalize0 (Safe_typing.push_context_set c) -let push_context c = globalize0 (Safe_typing.push_context c) +let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) +let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) @@ -249,7 +249,7 @@ let current_dirpath () = let with_global f = let (a, ctx) = f (env ()) (current_dirpath ()) in - push_context_set ctx; a + push_context_set false ctx; a (* spiwack: register/unregister functions for retroknowledge *) let register field value by_clause = |