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 +++-
 test-suite/bugs/closed/shouldsucceed/2608.v | 34 +++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2608.v

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'
diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/shouldsucceed/2608.v
new file mode 100644
index 0000000000..a4c95ff97c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2608.v
@@ -0,0 +1,34 @@
+
+Module Type T.
+  Parameter Inline t : Type.
+End T.
+
+Module M.
+  Definition t := nat.
+End M.
+
+Module Make (X:T).
+  Include X.
+
+  (* here t is : (Top.Make.t,Top.X.t) *)
+
+  (* in libobject HEAD : EvalConstRef (Top.X.t,Top.X.t)
+     which is substituted by : {Top.X |-> Top.Make [, Top.Make.t=>Top.X.t]}
+     which gives : EvalConstRef (Top.Make.t,Top.X.t) *)
+
+End Make.
+
+Module P := Make M.
+
+  (* resolver returned by add_module : Top.P.t=>inline *)
+  (* then constant_of_delta_kn P.t produces (Top.P.t,Top.P.t) *)
+
+  (* in libobject HEAD : EvalConstRef (Top.Make.t,Top.X.t)
+     given to subst = {<X#1> |-> Top.M [, Top.M.t=>inline]}
+     which used to give : EvalConstRef (Top.Make.t,Top.M.t)
+     given to subst = {Top.Make |-> Top.P [, Top.P.t=>inline]}
+     which used to give : EvalConstRef (Top.P.t,Top.M.t) *)
+
+Definition u := P.t.
+ (* was raising Not_found since Heads.head_map knows of (Top.P.t,Top.M.t)
+    and not of (Top.P.t,Top.P.t) *)
-- 
cgit v1.2.3