Adapt to rocq-prover/rocq#21391.

Author: ppedrot

src/run.ml

@@ -1246,8 +1246,9 @@ let declare_mind env sigma params sigs mut_constrs =
   let univs, ubinders = Evd.univ_entry ~poly:false sigma in
   let uctx = match univs with
     | UState.Monomorphic_entry ctx ->
-        let () = Global.push_context_set QGraph.Internal ctx in
-        Entries.Monomorphic_ind_entry
+      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
+      Entries.Monomorphic_ind_entry
     | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
   in
   let _ = DeclareInd.declare_mutual_inductive_with_eliminations