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/cooking.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index fdcf44c943..cb33bb729c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -38,13 +38,13 @@ struct
   type t = my_global_reference
   let equal gr1 gr2 = match gr1, gr2 with
   | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
-  | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
+  | IndRef i1, IndRef i2 -> Ind.SyntacticOrd.equal i1 i2
   | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
   | _ -> false
   open Hashset.Combine
   let hash = function
   | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
-  | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
+  | IndRef i -> combinesmall 2 (Ind.SyntacticOrd.hash i)
   | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
 end
 
-- 
cgit v1.2.3