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
---
 tactics/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index fb06bb8a4f..da4de3df77 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -56,7 +56,7 @@ let declare_universe_context ~poly ctx =
     let nas = name_instance (Univ.UContext.instance uctx) in
     Global.push_section_context (nas, uctx)
   else
-    Global.push_context_set false ctx
+    Global.push_context_set ~strict:true ctx
 
 (** Declaration of constants and parameters *)
 
-- 
cgit v1.2.3