diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 227a4f9ed0..cb6146338c 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -163,7 +163,7 @@ let new_Type_sort () = Type (new_univ ()) let refresh_universes_gen strict t = let modified = ref false in let rec refresh t = match kind_of_term t with - | Sort (Type u) when strict or u <> Univ.lower_univ -> + | Sort (Type u) when strict or u <> Univ.type0m_univ -> modified := true; new_Type () | Prod (na,u,v) -> mkProd (na,u,refresh v) | _ -> t in |