Merge pull request Mtac2#415 from jrosain/elimination-constraints

Adapt to rocq-prover/rocq#21195 (add quality constraint kinds)

Author: Janno

src/metaCoqInterp.ml

@@ -43,7 +43,7 @@ let glob_mtac_type ist r =
           (* need to instantiate and register the abstract universes a *)
           let inst, ctx = UnivGen.fresh_instance_from au None in
           (* TODO: find out why UnivFlexible needs a bool & select correct bool. *)
-          let sigma = Evd.merge_sort_context_set ?sideff:(Some false) (Evd.UnivFlexible true) sigma ctx in
+          let sigma = Evd.merge_sort_context_set ?sideff:(Some false) (Evd.UnivFlexible true) QGraph.Internal sigma ctx in
           sigma, Vars.subst_instance_constr inst ty, (fun ty -> PolyProgram (au, ty))
     in
     let ty = EConstr.of_constr ty in
@@ -200,7 +200,7 @@ module MetaCoqRun = struct
               try
                 let inst, ctx = UnivGen.fresh_instance_from au None in
                 (* TODO: find out why UnivFlexible needs a bool & select correct bool. *)
-                let sigma = Evd.merge_sort_context_set ?sideff:(Some false) (Evd.UnivFlexible true) sigma ctx in
+                let sigma = Evd.merge_sort_context_set ?sideff:(Some false) (Evd.UnivFlexible true) QGraph.Internal sigma ctx in
                 let sigma = Evarconv.unify_leq_delay env sigma concl ty in
                 ((false, sigma, ty, EConstr.UnsafeMonomorphic.mkConst c), None)
               with Evarconv.UnableToUnify(_,_) -> CErrors.user_err (Pp.str "Different types")

src/run.ml

@@ -1246,7 +1246,7 @@ 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 ctx in
+        let () = Global.push_context_set QGraph.Internal ctx in
         Entries.Monomorphic_ind_entry
     | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
   in