Adapt to rocq-prover/rocq#21394.

Author: ppedrot

src/principles.ml

@@ -1691,8 +1691,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_qualities QGraph.Internal (PConstraints.ContextSet.sort_context_set ctx) in (* XXX *)
-      let () = Global.push_context_set (PConstraints.ContextSet.univ_context_set ctx) in
+      let () = Global.push_context_set ctx in
       Entries.Monomorphic_ind_entry
     | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
     in

src/subterm.ml

@@ -153,8 +153,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_qualities QGraph.Internal (PConstraints.ContextSet.sort_context_set ctx) in (* XXX *)
-    let () = Global.push_context_set (PConstraints.ContextSet.univ_context_set ctx) in
+    let () = Global.push_context_set ctx in
     Entries.Monomorphic_ind_entry
   | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
   in