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

(limited to 'checker')

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index ef606c9a75..7bb714aa17 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -104,7 +104,7 @@ let check_kelim k1 k2 = Sorts.family_leq k1 k2
 let eq_nested_types ty1 ty2 = match ty1, ty2 with
 | NestedInd ind1, NestedInd ind2 -> eq_ind_chk ind1 ind2
 | NestedInd _, _ -> false
-| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2
+| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2
 | NestedPrimitive _, _ -> false
 
 let eq_recarg a1 a2 = match a1, a2 with
-- 
cgit v1.2.3