aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativevalues.ml')
-rw-r--r--kernel/nativevalues.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 05c98e4b87..bd6241ae67 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -36,13 +36,13 @@ type annot_sw = {
(* We compare only what is relevant for generation of ml code *)
let eq_annot_sw asw1 asw2 =
- eq_ind asw1.asw_ind asw2.asw_ind &&
+ Ind.CanOrd.equal asw1.asw_ind asw2.asw_ind &&
String.equal asw1.asw_prefix asw2.asw_prefix
open Hashset.Combine
let hash_annot_sw asw =
- combine (ind_hash asw.asw_ind) (String.hash asw.asw_prefix)
+ combine (Ind.CanOrd.hash asw.asw_ind) (String.hash asw.asw_prefix)
type sort_annot = string * int