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

4 files changed, 20 insertions, 8 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 257bd43083..bd5a000c2b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -296,7 +296,13 @@ val add_constraints : Univ.Constraint.t -> env -> env
 (** Check constraints are satifiable in the environment. *)
 val check_constraints : Univ.Constraint.t -> env -> bool
 val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
+(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment.
+   @raise UGraph.AlreadyDeclared if one of the universes is already declared.
+*)
 val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
+(* [push_context_set ?(strict=false) ctx env] pushes the universe context set
+  to the environment. It does not fail if one of the universes is already declared. *)
+
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val push_subgraph : Univ.ContextSet.t -> env -> env
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c91cb39fe2..a14d10c841 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -351,8 +351,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
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 759feda9ab..d45cfcab78 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -331,13 +331,13 @@ type constraints_addition =
   | Now of Univ.ContextSet.t
   | Later of Univ.ContextSet.t Future.computation
 
-let push_context_set poly cst senv =
+let push_context_set ~strict cst senv =
   if Univ.ContextSet.is_empty cst then senv
   else
     let sections = Option.map (Section.push_constraints cst) senv.sections
     in
     { senv with
-      env = Environ.push_context_set ~strict:(not poly) cst senv.env;
+      env = Environ.push_context_set ~strict cst senv.env;
       univ = Univ.ContextSet.union cst senv.univ;
       sections }
 
@@ -346,7 +346,7 @@ let add_constraints cst senv =
   | Later fc ->
     {senv with future_cst = fc :: senv.future_cst}
   | Now cst ->
-    push_context_set false cst senv
+    push_context_set ~strict:true cst senv
 
 let add_constraints_list cst senv =
   List.fold_left (fun acc c -> add_constraints c acc) senv cst
@@ -547,7 +547,7 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
     else
       (* Delayed constraints from opaque body are added by [add_constant_aux] *)
       let cst = constraints_of_sfb sfb in
-      List.fold_left (fun senv cst -> push_context_set false cst senv) senv cst
+      List.fold_left (fun senv cst -> push_context_set ~strict:true cst senv) senv cst
   in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -998,7 +998,7 @@ let close_section senv =
   let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in
   let senv = { senv with env; revstruct; sections; univ; objlabels; } in
   (* Second phase: replay the discharged section contents *)
-  let senv = push_context_set false cstrs senv in
+  let senv = push_context_set ~strict:true cstrs senv in
   let modlist = Section.replacement_context env0 sections0 in
   let cooking_info seg =
     let { abstr_ctx; abstr_subst; abstr_uctx } = seg in
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