From 4585baa53e7fa4c25e304b8136944748a7622e10 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 18:42:38 +0200 Subject: 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. --- library/global.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library/global.ml') 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 = -- cgit v1.2.3