Skip to content

Commit 7886ea4

Browse files
committed
Adapt to rocq-prover/rocq#21395 (revert univ_decl name change)
1 parent 64a6980 commit 7886ea4

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr
4242
let ctor_type_to_constr cty =
4343
EConstr.to_constr sigma (EConstr.Vars.subst_var sigma name cty)
4444
in
45-
let univs, ubinders = Evd.check_sort_poly_decl ~poly:false sigma UState.default_sort_poly_decl in
45+
let univs, ubinders = Evd.check_univ_decl ~poly:false sigma UState.default_univ_decl in
4646
let uctx = match univs with
4747
| UState.Monomorphic_entry ctx ->
4848
let () = Global.push_context_set ctx in

0 commit comments

Comments
 (0)