diff --git a/src/principles.ml b/src/principles.ml
index 4f9d93fb..018b4f80 100644
--- a/src/principles.ml
+++ b/src/principles.ml
@@ -1690,7 +1690,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
     let univs, ubinders = Evd.univ_entry ~poly sigma in
     let uctx = match univs with
     | UState.Monomorphic_entry ctx ->
-      let () = Global.push_context_set ~strict:true ctx in
+      let () = Global.push_context_set ctx in
       Entries.Monomorphic_ind_entry
     | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
     in
@@ -1759,7 +1759,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
     if not poly then
       (* Declare the universe context necessary to typecheck the following
           definitions once and for all. *)
-      (Global.push_context_set ~strict:true (Evd.universe_context_set !evd);
+      (Global.push_context_set (Evd.universe_context_set !evd);
        evd := Evd.from_env (Global.env ()))
     else ()
   in
diff --git a/src/subterm.ml b/src/subterm.ml
index 82927541..93cdd8a8 100644
--- a/src/subterm.ml
+++ b/src/subterm.ml
@@ -152,7 +152,7 @@ let derive_subterm ~pm env sigma ~poly (ind, u as indu) =
   let univs, ubinders = Evd.univ_entry ~poly sigma in
   let uctx = match univs with
   | UState.Monomorphic_entry ctx ->
-    let () = Global.push_context_set ~strict:true ctx in
+    let () = Global.push_context_set ctx in
     Entries.Monomorphic_ind_entry
   | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
   in