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

1 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/shouldsucceed/2608.v
new file mode 100644
index 000000000..a4c95ff97
--- /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) *)