Adapt to rocq-prover/rocq#21395 (revert univ_decl name change)

Author: SkySkimmer

src/equations.ml

@@ -163,7 +163,7 @@ let define_by_eqs ~pm ~poly ~program_mode ~tactic ~open_proof opts eqs nt =
   let evm, udecl =
     match eqs with
     | (((loc, i), udecl, _, _, _, _), _) :: _ ->
-      Constrintern.interp_sort_poly_decl_opt env udecl
+      Constrintern.interp_univ_decl_opt env udecl
     | _ -> assert false
   in
   let evd = ref evm in

src/g_equations.mlg

@@ -322,7 +322,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   proto:
-   [ [ id = lident; d = OPT sort_poly_decl; l = binders2; ":"; t = Constr.lconstr;
+   [ [ id = lident; d = OPT univ_decl; l = binders2; ":"; t = Constr.lconstr;
        reca = wf_annot; ":="; eqs = sub_equations -> { (fun r -> ((id, d, r, l, Some t, reca), eqs)) }
    ] ]
   ;

src/noconf_hom.ml

@@ -277,7 +277,7 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
       ~prefix:"Hom" ~tactic:(noconf_hom_tac ()) program_cst
  in
  let prog = Splitting.make_single_program env evd data.Covering.flags p ctxmap splitting None in
- Splitting.define_programs ~pm env evd UState.default_sort_poly_decl [None] [] data.Covering.flags [prog] hook
+ Splitting.define_programs ~pm env evd UState.default_univ_decl [None] [] data.Covering.flags [prog] hook
 
 let () =
   let derive_no_confusion_hom ~pm env sigma ~poly v =

src/principles.ml

@@ -1033,7 +1033,7 @@ let unfold_programs ~pm env evd flags rec_type progs =
       in
       let unfoldp = make_single_program env evd flags unfpi prob unfoldp.program_splitting None in
       let (unfoldp, term_info), pm, _pstate = define_program_immediate ~pm env evd 
-        UState.default_sort_poly_decl [None] [] flags ~unfold:true unfoldp in
+        UState.default_univ_decl [None] [] flags ~unfold:true unfoldp in
       let eqninfo =
         Principles_proofs.{ equations_id = i;
                             equations_where_map = where_map;

src/splitting.ml

@@ -1299,7 +1299,7 @@ let define_programs (type a) ~pm env evd udecl is_recursive fixprots flags ?(unf
   let all_hook ~pm hook recobls sigma =
     let sigma = Evd.minimize_universes sigma in
     let sigma = Evarutil.nf_evar_map_undefined sigma in
-    let uentry = UState.check_sort_poly_decl ~poly:flags.polymorphic (Evd.ustate sigma) udecl in
+    let uentry = UState.check_univ_decl ~poly:flags.polymorphic (Evd.ustate sigma) udecl in
     let () =
       if !Equations_common.debug then
         Feedback.msg_debug (str"Defining programs, before simplify_evars " ++ pr_programs env sigma programs);

src/splitting.mli

@@ -214,7 +214,7 @@ val define_programs :
   pm:Declare.OblState.t ->
   Environ.env ->
   Evd.evar_map ref ->
-  UState.sort_poly_decl ->
+  UState.universe_decl ->
   Syntax.rec_type ->
   EConstr.rel_context ->
   Equations_common.flags ->
@@ -227,7 +227,7 @@ val define_program_immediate :
   pm:Declare.OblState.t ->
   Environ.env ->
   Evd.evar_map ref ->
-  UState.sort_poly_decl ->
+  UState.universe_decl ->
   Syntax.rec_type ->
   EConstr.rel_context ->
   Equations_common.flags ->

src/syntax.ml

@@ -81,7 +81,7 @@ and ('a,'b) rhs_aux =
 and ('a,'b) rhs = ('a, 'b) rhs_aux option (* Empty patterns allow empty r.h.s. *)
 
 and pre_prototype =
-  identifier with_loc * Constrexpr.sort_poly_decl_expr option * user_rec_annot * 
+  identifier with_loc * Constrexpr.universe_decl_expr option * user_rec_annot *
   Constrexpr.local_binder_expr list * Constrexpr.constr_expr option *
   (Id.t with_loc option, Constrexpr.constr_expr * Constrexpr.constr_expr option) by_annot option
 

src/syntax.mli

@@ -72,7 +72,7 @@ and ('a,'b) rhs_aux =
   | Refine of Constrexpr.constr_expr list * 'b list
 and ('a,'b) rhs = ('a, 'b) rhs_aux option
 and pre_prototype =
-  identifier with_loc * Constrexpr.sort_poly_decl_expr option * user_rec_annot * 
+  identifier with_loc * Constrexpr.universe_decl_expr option * user_rec_annot *
   Constrexpr.local_binder_expr list * Constrexpr.constr_expr option *
   (Id.t with_loc option, Constrexpr.constr_expr * Constrexpr.constr_expr option) by_annot option