1 files changed, 40 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/1542.v b/test-suite/bugs/closed/1542.v
new file mode 100644
index 00000000..52cfbbc4
--- /dev/null
+++ b/test-suite/bugs/closed/1542.v
@@ -0,0 +1,40 @@
+Module Type TITI.
+Parameter B:Set.
+Parameter x:B.
+Inductive A:Set:=
+a1:B->A.
+Definition f2: A ->B
+:= fun (a:A) =>
+match a with
+ (a1 b)=>b
+end.
+Definition f: A -> B:=fun (a:A) => x.
+End TITI.
+
+
+Module Type TIT.
+Declare Module t:TITI.
+End TIT.
+
+Module Seq(titi:TIT).
+Module t:=titi.t.
+Inductive toto:t.A->t.B->Set:=
+t1:forall (a:t.A), (toto a (t.f a))
+| t2:forall (a:t.A), (toto a (t.f2 a)).
+End Seq.
+
+Module koko(tit:TIT).
+Module seq:=Seq tit.
+Module t':=tit.t.
+
+Definition def:forall (a:t'.A), (seq.toto a (t'.f a)).
+intro ; constructor 1.
+Defined.
+
+Definition def2: forall (a:t'.A), (seq.toto a (t'.f2 a)).
+intro; constructor 2.
+(*  Toplevel input, characters 0-13
+  constructor 2.
+  ^^^^^^^^^^^^^
+Error: Impossible to unify (seq.toto ?3 (seq.t.f2 ?3)) with
+ (seq.toto a (t'.f2 a)).*)