From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/bugs/closed/1542.v | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 test-suite/bugs/closed/1542.v (limited to 'test-suite/bugs/closed/1542.v') 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)).*) -- cgit v1.2.3