diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d6bc6eb717..55b82e2148 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -615,10 +615,10 @@ let sort_cmp = sort_cmp let base_sort_cmp pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) -> c1 = c2 + | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos (* Prop <= Set *) | (Prop c1, Type u) -> pb = CUMUL | (Type u1, Type u2) -> true - | (Type u, Prop _) -> u = lower_univ & pb = CUMUL + | _ -> false let test_conversion f env sigma x y = 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 |