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
---
 kernel/safe_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 0b7ca26e09..92bbd264fa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -113,7 +113,7 @@ val add_modtype :
 (** Adding universe constraints *)
 
 val push_context_set :
-  bool -> Univ.ContextSet.t -> safe_transformer0
+  strict:bool -> Univ.ContextSet.t -> safe_transformer0
 
 val add_constraints :
   Univ.Constraint.t -> safe_transformer0
-- 
cgit v1.2.3