From 12a77d49db68f88fc5886d6527217a761045865b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 25 Mar 2015 11:15:51 +0100
Subject: Use kernel names instead of user names when looking for coercions.
 (Fix for bug #4133)

Note that, if someone was purposely modifying the user name of a type in
order to disable a coercion, it no longer works. Hopefully, no one did.
---
 pretyping/classops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 559f5fe66a..055996de55 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -60,9 +60,9 @@ let coe_info_typ_equal c1 c2 =
 
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
-  | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> con_user_ord c1 c2
-  | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2
+  | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2
+  | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
   | _ -> Pervasives.compare t1 t2 (** OK *)
 
 module ClTyp = struct
-- 
cgit v1.2.3