Adapt to rocq-prover/rocq#21394. (#185)

Author: ppedrot

src/Rewriter/Util/plugins/inductive_from_elim.ml.v92

@@ -45,8 +45,7 @@ let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr
     let univs, ubinders = Evd.check_sort_poly_decl ~poly:false sigma UState.default_sort_poly_decl in
     let uctx = match univs with
     | UState.Monomorphic_entry ctx ->
-      let () = Global.push_qualities QGraph.Internal (PConstraints.ContextSet.sort_context_set ctx) in
-      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