From 63710768d32c5929aa6498aff5aae2f9e0058e95 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 24 Oct 2011 23:07:14 +0000
Subject: Mod_subst: Attempt to fix #2608

 In presence of inlining, it seems that no alias is propagated
 on the canonical kernel_name. We modify [subst_con0] to enforce
 this semantics. It seems to work well, but my understanding of
 this code is still limited...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14587 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_subst.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f32198f800..668f2d412e 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -295,7 +295,9 @@ let subst_con0 sub con =
   let dup con = con, mkConst con in
   let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
   match constant_of_delta_with_inline resolve con' with
-    | Some t -> con', t
+    | Some t ->
+      (* In case of inlining, discard the canonical part (cf #2608) *)
+      constant_of_kn (user_con con'), t
     | None ->
       let con'' = match side with
 	| User -> constant_of_delta resolve con'
-- 
cgit v1.2.3