Merge pull request #1150 from SkySkimmer/clean-univ

Adapt to rocq-prover/rocq#20360 (pr_universe_context_set renamed)

Author: ppedrot

template-coq/src/quoter.ml

@@ -231,7 +231,7 @@ struct
         eqs (levels, cstrs)
     in
     let levels = Univ.Level.Set.add Univ.Level.set levels in
-    debug Pp.(fun () -> str"Universe context: " ++ Univ.pr_universe_context_set Univ.Level.raw_pr (levels, cstrs));
+    debug Pp.(fun () -> str"Universe context: " ++ Univ.ContextSet.pr Univ.Level.raw_pr (levels, cstrs));
     time (Pp.str"Quoting universe context")
       (fun uctx -> Q.quote_univ_contextset uctx) (levels, cstrs)
 

template-coq/src/run_template_monad.ml

@@ -312,7 +312,7 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool
   let evm, mind =
     if infer_univs then
       let ctx, mind = Tm_util.RetypeMindEntry.infer_mentry_univs env evm' mind in
-      debug (fun () -> Pp.(str "Declaring universe context " ++ Univ.pr_universe_context_set UnivNames.pr_level_with_global_universes ctx));
+      debug (fun () -> Pp.(str "Declaring universe context " ++ Univ.ContextSet.pr UnivNames.pr_level_with_global_universes ctx));
       Global.push_context_set ctx;
       Evd.merge_context_set Evd.UnivRigid evm ctx, mind
     else evm, mind