1 files changed, 0 insertions, 34 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/shouldsucceed/2608.v
deleted file mode 100644
index a4c95ff9..00000000
--- a/test-suite/bugs/closed/shouldsucceed/2608.v
+++ /dev/null
@@ -1,34 +0,0 @@
-
-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) *)