diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-11 17:06:13 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-11 17:28:56 +0100 |
commit | ac65eef8bbc2e405f1964f35c6a129dfa1755888 (patch) | |
tree | d948c59c8fa70d905ca443e7bac8b944f6d8a7a9 /checker/univ.ml | |
parent | e8af74ad7913773c4dfb688167b15b6e15e4397a (diff) |
Fixing bug #4019, and checker blow-up at once.
Diffstat (limited to 'checker/univ.ml')
-rw-r--r-- | checker/univ.ml | 20 |
1 files changed, 15 insertions, 5 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 } |