From 3c24d4f6398cc80fd070c4e6dcac99670c8c1bba Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 13 Dec 2019 11:40:48 +0100
Subject: Use ~strict argument consistently in push_context/push_context_set
 intfs

One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
---
 library/global.ml  | 4 ++--
 library/global.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index d4262683bb..fbbe09301b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -90,7 +90,7 @@ 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 push_section_context c = globalize0 (Safe_typing.push_section_context c)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
-let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
+let push_context_set ~strict c = globalize0 (Safe_typing.push_context_set ~strict c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
@@ -206,7 +206,7 @@ let current_dirpath () =
 
 let with_global f =
   let (a, ctx) = f (env ()) (current_dirpath ()) in
-    push_context_set false ctx; a
+  push_context_set ~strict:true ctx; a
 
 let register_inline c = globalize0 (Safe_typing.register_inline c)
 let register_inductive c r = globalize0 (Safe_typing.register_inductive c r)
diff --git a/library/global.mli b/library/global.mli
index db0f87df7e..a38fde41a5 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -60,7 +60,7 @@ val add_mind :
 (** Extra universe constraints *)
 val add_constraints : Univ.Constraint.t -> unit
 
-val push_context_set : bool -> Univ.ContextSet.t -> unit
+val push_context_set : strict:bool -> Univ.ContextSet.t -> unit
 
 (** Non-interactive modules and module types *)
 
-- 
cgit v1.2.3