aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-27 12:55:13 +0000
committerGitHub2020-10-27 12:55:13 +0000
commit5f5cddae48c08872107f30938dcc2f3c8d91f33a (patch)
tree2f1bb58c33fee5b4bb0913296ef4341a8832feb4 /kernel/nativevalues.ml
parentb87fd6cfe5fe872a38d98c294aea84cde8c6c160 (diff)
parent375fc707b402b855770ec32c57ad1362f2a89e5c (diff)
Merge PR #13075: Introducing the foundations for a name-alias-agnostic API
Reviewed-by: SkySkimmer Ack-by: gares Ack-by: ejgallego
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