diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-04 20:21:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-04 20:23:19 +0200 |
| commit | bd0e8ce51ed8eb8359d198fb5d14d14381847200 (patch) | |
| tree | 1dbb836ca2d2a696196394573ac4c7225c454723 /checker/closure.ml | |
| parent | f65fa9de8a4c9c12d933188a755b51508bd51921 (diff) | |
Fixing coqchk. It was my fault, I misused canonical and user equalities
when defining cache hash tables in Closure. Why it was working in 3.12
is a mystery to me.
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 6248b440f..831f50454 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -169,7 +169,7 @@ module KeyHash = struct type t = table_key let equal k1 k2 = match k1, k2 with - | ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 + | ConstKey c1, ConstKey c2 -> Constant.UserOrd.equal c1 c2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey i1, RelKey i2 -> Int.equal i1 i2 | (ConstKey _ | VarKey _ | RelKey _), _ -> false @@ -177,7 +177,7 @@ struct open Hashset.Combine let hash = function - | ConstKey c -> combinesmall 1 (Constant.hash c) + | ConstKey c -> combinesmall 1 (Constant.UserOrd.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) end |