Merge pull request #630 from SkySkimmer/set-leq-noenv

Adapt to coq/coq#20069 (set_leq_sort doesn't need an env)
mattam82 · Jan 23, 2025 · eb85124 · eb85124
2 parents 3431c88 + 4d4d3e5
commit eb85124
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/equations_common.ml b/src/equations_common.ml
@@ -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 =