From cd139311ecd872301077b9db2df812a828ce2e77 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 21:34:38 +0200
Subject: Fixing an incompatility introduced in a404360: kernel conversion was
 not considering conversion of constants over their canonical name but on
 their user name. This is observable when delta is off.

---
 kernel/reduction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 97c3e1b348..2f1df396b5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -193,7 +193,7 @@ let convert_instances ~flex u u' (s, check) =
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
   match k1, k2 with
-  | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' ->
+  | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' ->
     if Univ.Instance.equal u u' then cuniv
     else 
       let flex = evaluable_constant cst (info_env infos) 
-- 
cgit v1.2.3