From bd0e8ce51ed8eb8359d198fb5d14d14381847200 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Apr 2014 20:21:06 +0200
Subject: 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.

---
 checker/closure.ml | 4 ++--
 kernel/closure.ml  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/checker/closure.ml b/checker/closure.ml
index 6248b440ff..831f504545 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
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 55b0384823..7b94ecfb85 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -214,7 +214,7 @@ struct
   let equal = Names.eq_id_key
   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
-- 
cgit v1.2.3