diff options
author | 2015-02-11 17:06:13 +0100 | |
---|---|---|
committer | 2015-02-11 17:28:56 +0100 | |
commit | ac65eef8bbc2e405f1964f35c6a129dfa1755888 (patch) | |
tree | d948c59c8fa70d905ca443e7bac8b944f6d8a7a9 | |
parent | e8af74ad7913773c4dfb688167b15b6e15e4397a (diff) |
Fixing bug #4019, and checker blow-up at once.
-rw-r--r-- | checker/univ.ml | 20 | ||||
-rw-r--r-- | kernel/univ.ml | 22 |
2 files changed, 31 insertions, 11 deletions
diff --git a/checker/univ.ml b/checker/univ.ml index 8d0ae8f1e..3bcb3bc95 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -174,6 +174,16 @@ struct | _, Level _ -> 1 | Var n, Var m -> Int.compare n m + let hequal x y = + x == y || + match x, y with + | Prop, Prop -> true + | Set, Set -> true + | Level (n,d), Level (n',d') -> + n == n' && d == d' + | Var n, Var n' -> n == n' + | _ -> false + let hcons = function | Prop as x -> x | Set as x -> x @@ -218,17 +228,17 @@ module Level = struct module Self = struct type _t = t type t = _t - type u = raw_level -> raw_level - let equal x y = x.hash == y.hash && x.data == y.data + type u = unit + let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash - let hashcons hraw x = - let data' = hraw x.data in + let hashcons () x = + let data' = RawLevel.hcons x.data in if x.data == data' then x else { x with data = data' } end let hcons = let module H = Hashcons.Make(Self) in - Hashcons.simple_hcons H.generate H.hcons RawLevel.hcons + Hashcons.simple_hcons H.generate H.hcons () let make l = hcons { hash = RawLevel.hash l; data = l } diff --git a/kernel/univ.ml b/kernel/univ.ml index ea5727620..763c0822f 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -194,7 +194,17 @@ struct | Level _, _ -> -1 | _, Level _ -> 1 | Var n, Var m -> Int.compare n m - + + let hequal x y = + x == y || + match x, y with + | Prop, Prop -> true + | Set, Set -> true + | Level (n,d), Level (n',d') -> + n == n' && d == d' + | Var n, Var n' -> n == n' + | _ -> false + let hcons = function | Prop as x -> x | Set as x -> x @@ -240,17 +250,17 @@ module Level = struct module Self = struct type _t = t type t = _t - type u = raw_level -> raw_level - let equal x y = x.hash == y.hash && x.data == y.data + type u = unit + let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash - let hashcons hraw x = - let data' = hraw x.data in + let hashcons () x = + let data' = RawLevel.hcons x.data in if x.data == data' then x else { x with data = data' } end let hcons = let module H = Hashcons.Make(Self) in - Hashcons.simple_hcons H.generate H.hcons RawLevel.hcons + Hashcons.simple_hcons H.generate H.hcons () let make l = hcons { hash = RawLevel.hash l; data = l } |