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.
---
 library/coqlib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/coqlib.ml')

diff --git a/library/coqlib.ml b/library/coqlib.ml
index b374ecbca0..82d1ecacb5 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -45,7 +45,7 @@ let has_ref s = CString.Map.mem s !table
 
 let check_ind_ref s ind =
   match CString.Map.find s !table with
-  | GlobRef.IndRef r -> eq_ind r ind
+  | GlobRef.IndRef r -> Ind.CanOrd.equal r ind
   | _ -> false
   | exception Not_found -> false
 
-- 
cgit v1.2.3