Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~strict flag

Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot

1 files changed, 8 insertions, 2 deletions

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 982bc49927..d9ccf81619 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -293,8 +293,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   let env_univs =
     match mie.mind_entry_universes with
     | Monomorphic_entry ctx ->
-      let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in
-      push_context_set ctx env
+      if has_template_poly then
+        (* For that particular case, we typecheck the inductive in an environment
+           where the universes introduced by the definition are only [>= Prop] *)
+        let env = set_universes_lbound env Univ.Level.prop in
+        push_context_set ~strict:false ctx env
+      else
+        (* In the regular case, all universes are [> Set] *)
+        push_context_set ~strict:true ctx env
     | Polymorphic_entry (_, ctx) -> push_context ctx env
   in