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

9 files changed, 36 insertions, 24 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
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 *)
 
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 *)
 
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 54dda09e83..c816a4eb4f 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -550,7 +550,7 @@ let intern_arg (acc, cst) (idl,(typ,ann)) =
   let lib_dir = Lib.library_dp() in
   let env = Global.env() in
   let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in
-  let () = Global.push_context_set true cst' in
+  let () = Global.push_context_set ~strict:true cst' in
   let env = Global.env () in
   let sobjs = get_module_sobjs false env inl mty in
   let mp0 = get_module_path mty in
@@ -674,7 +674,7 @@ module RawModOps = struct
 let start_module export id args res fs =
   let mp = Global.start_module id in
   let arg_entries_r, cst = intern_args args in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   let env = Global.env () in
   let res_entry_o, subtyps, cst = match res with
     | Enforce (res,ann) ->
@@ -689,7 +689,7 @@ let start_module export id args res fs =
       let typs, cst = build_subtypes env mp arg_entries_r resl in
       None, typs, cst
   in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
   Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix));
@@ -782,7 +782,7 @@ let declare_module id args res mexpr_o fs =
   | None -> None
   | _ -> inl_res
   in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   let mp_env,resolver = Global.add_module id entry inl in
 
   (* Name consistency check : kernel vs. library *)
@@ -804,10 +804,10 @@ module RawModTypeOps = struct
 let start_modtype id args mtys fs =
   let mp = Global.start_modtype id in
   let arg_entries_r, cst = intern_args args in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   let env = Global.env () in
   let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix));
@@ -835,19 +835,19 @@ let declare_modtype id args mtys (mty,ann) fs =
      then we adds the module parameters to the global env. *)
   let mp = Global.start_modtype id in
   let arg_entries_r, cst = intern_args args in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
   let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   let env = Global.env () in
   (* We check immediately that mte is well-formed *)
   let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   let env = Global.env () in
   let entry = params, mte in
   let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   let env = Global.env () in
   let sobjs = get_functor_sobjs false env inl entry in
   let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
@@ -903,7 +903,7 @@ let type_of_incl env is_mod = function
 let declare_one_include (me_ast,annot) =
   let env = Global.env() in
   let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in
-  let () = Global.push_context_set true cst in
+  let () = Global.push_context_set ~strict:true cst in
   let env = Global.env () in
   let is_mod = (kind == Modintern.Module) in
   let cur_mp = Lib.current_mp () in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e4965614d8..439ec61d38 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1621,7 +1621,7 @@ let vernac_global_check c =
   let c,uctx = interp_constr env sigma c in
   let senv = Global.safe_env() in
   let uctx = UState.context_set uctx in
-  let senv = Safe_typing.push_context_set false uctx senv in
+  let senv = Safe_typing.push_context_set ~strict:false uctx senv in
   let c = EConstr.to_constr sigma c in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in