Skip to content

Adapt to rocq-prover/rocq#21820 (collapse_sort_variables arg change) #196

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
JasonGross merged 1 commit into from
Apr 1, 2026
Merged

Adapt to rocq-prover/rocq#21820 (collapse_sort_variables arg change) #196

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Rewriter/Util/plugins/inductive_from_elim.ml.v93
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr
let ctor_type_to_constr cty =
EConstr.to_constr sigma (EConstr.Vars.subst_var sigma name cty)
in
let sigma = Evd.collapse_sort_variables sigma in
let sigma = Evd.collapse_sort_variables ~only_above_prop:false sigma in
let univs, ubinders = Evd.check_univ_decl ~poly:PolyFlags.default sigma UState.default_univ_decl in
let uctx = match univs with
| UState.Monomorphic_entry ctx ->
Expand Down
Loading