From bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 12:42:21 +0200
Subject: Introduce an Ind module in the Names API.

This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
---
 kernel/nativevalues.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/nativevalues.ml')

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
 
-- 
cgit v1.2.3