aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmvalues.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vmvalues.ml')
-rw-r--r--kernel/vmvalues.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 2068133b10..28a7abc7c6 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -250,7 +250,7 @@ type id_key =
| EvarKey of Evar.t
let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with
-| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2
+| ConstKey c1, ConstKey c2 -> Constant.CanOrd.equal c1 c2
| VarKey id1, VarKey id2 -> Id.equal id1 id2
| RelKey n1, RelKey n2 -> Int.equal n1 n2
| EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2
@@ -469,7 +469,7 @@ struct
let equal = eq_id_key
open Hashset.Combine
let hash : t -> tag = function
- | ConstKey c -> combinesmall 1 (Constant.hash c)
+ | ConstKey c -> combinesmall 1 (Constant.CanOrd.hash c)
| VarKey id -> combinesmall 2 (Id.hash id)
| RelKey i -> combinesmall 3 (Int.hash i)
| EvarKey evk -> combinesmall 4 (Evar.hash evk)