Skip to content

Commit

Permalink
Adapt to coq/coq#20069 (set_leq_sort doesn't need an env)
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Jan 22, 2025
1 parent 3431c88 commit 4d4d3e5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/equations_common.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1104,7 +1104,7 @@ let nonalgebraic_universe_level_of_universe env sigma u =
| None ->
let sigma, l = Evd.new_univ_level_variable Evd.univ_flexible sigma in
let ul = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make l in
let sigma = Evd.set_leq_sort env sigma u ul in
let sigma = Evd.set_leq_sort sigma u ul in
sigma, l, ul

let instance_of env sigma ?argu goalu =
Expand Down

0 comments on commit 4d4d3e5

Please sign in to comment.