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

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index fc6afb79d4..00418009c7 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -83,7 +83,7 @@ and conv_atom env pb lvl a1 a2 cu =
        if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
        else raise NotConvertible
     | Aconstant (c1,u1), Aconstant (c2,u2) ->
-       if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
+       if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
        else raise NotConvertible
     | Asort s1, Asort s2 ->
         sort_cmp_universes env pb s1 s2 cu
-- 
cgit v1.2.3