diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 15 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 6 | ||||
| -rw-r--r-- | pretyping/termops.ml | 6 |
3 files changed, 8 insertions, 19 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e825b3f488..d7573b5342 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -611,25 +611,14 @@ let pb_equal = function | CUMUL -> CONV | CONV -> CONV -let sort_cmp pb s0 s1 cuniv = - match (s0,s1) with - | (Prop c1, Prop c2) -> if c1 = c2 then cuniv else raise NotConvertible - | (Prop c1, Type u) -> - (match pb with - CUMUL -> cuniv - | _ -> raise NotConvertible) - | (Type u1, Type u2) -> - (match pb with - | CONV -> enforce_eq u1 u2 cuniv - | CUMUL -> enforce_geq u2 u1 cuniv) - | (_, _) -> raise NotConvertible +let sort_cmp = sort_cmp let base_sort_cmp pb s0 s1 = match (s0,s1) with | (Prop c1, Prop c2) -> c1 = c2 | (Prop c1, Type u) -> pb = CUMUL | (Type u1, Type u2) -> true - | (_, _) -> false + | (Type u, Prop _) -> u = lower_univ & pb = CUMUL let test_conversion f env sigma x y = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 635a579c05..795627fc41 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -84,7 +84,7 @@ let retype sigma metamap = and sort_of env t = match kind_of_term t with | Cast (c,_, s) when isSort s -> destSort s - | Sort (Prop c) -> type_0 + | Sort (Prop c) -> type1_sort | Sort (Type u) -> Type (Univ.super u) | Prod (name,t,c2) -> (match (sort_of env t, sort_of (push_rel (name,None,t) env) c2) with @@ -92,8 +92,8 @@ let retype sigma metamap = | Prop _, (Prop Pos as s) -> s | Type _, (Prop Pos as s) when Environ.engagement env = Some ImpredicativeSet -> s - | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.base_univ) - | Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2) + | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ) + | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) | App(f,args) when isGlobalRef f -> diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 01104a8156..a81f68b79d 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -163,15 +163,15 @@ let new_Type_sort () = Type (new_univ ()) let refresh_universes t = let modified = ref false in let rec refresh t = match kind_of_term t with - | Sort (Type _) -> modified := true; new_Type () + | Sort (Type u) when u <> Univ.lower_univ -> modified := true; new_Type () | Prod (na,u,v) -> mkProd (na,u,refresh v) | _ -> t in let t' = refresh t in if !modified then t' else t let new_sort_in_family = function - | InProp -> mk_Prop - | InSet -> mk_Set + | InProp -> prop_sort + | InSet -> set_sort | InType -> Type (new_univ ()) |