diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 8afb9b942..3f5d186d4 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -69,7 +69,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if onlyalg && alg then (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) - | Prop Pos when refreshset && not direction -> + | Set when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) refresh_sort status ~direction s |