Imported Upstream version 8.3.pl3upstream/8.3.pl3

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 00000000..a4c95ff9
--- /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) *)