Skip to content

Commit

Permalink
Fix set_leq_sort
Browse files Browse the repository at this point in the history
  • Loading branch information
mattam82 committed Jan 28, 2025
1 parent 2a04352 commit 72484f2
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/equations_common.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1090,10 +1090,10 @@ let evd_comb1 f evd x =

(* Universe related functions *)

[%%if rocq = "9.0"]
let set_leq_sort env = Evd.set_leq_sort
[%%if rocq = "9.1"]
let set_leq_sort _ = Evd.set_leq_sort
[%%else]
let set_leq_sort env = Evd.set_leq_sort
let set_leq_sort env = Evd.set_leq_sort env
[%%endif]

let nonalgebraic_universe_level_of_universe env sigma u =
Expand Down

0 comments on commit 72484f2

Please sign in to comment.