From 2b91a8989687e152f7120aa6c907ffeba8495bab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 10:44:51 +0200
Subject: Deprecate the non-qualified equality functions on kerpairs.

This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
---
 kernel/primred.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/primred.ml')

diff --git a/kernel/primred.ml b/kernel/primred.ml
index f158cfacea..17e5a89b74 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -12,7 +12,7 @@ type _ action_kind =
 type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
 
 let check_same_types typ c1 c2 =
-  if not (Constant.equal c1 c2)
+  if not (Constant.CanOrd.equal c1 c2)
   then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
 
 let check_same_inds ind i1 i2 =
-- 
cgit v1.2.3


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

(limited to 'kernel/primred.ml')

diff --git a/kernel/primred.ml b/kernel/primred.ml
index 17e5a89b74..f0b4d6d362 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -16,7 +16,7 @@ let check_same_types typ c1 c2 =
   then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
 
 let check_same_inds ind i1 i2 =
-  if not (eq_ind i1 i2)
+  if not (Ind.CanOrd.equal i1 i2)
   then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2))
 
 let add_retroknowledge retro action =
-- 
cgit v1.2.3