summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/328.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/328.v')
-rw-r--r--test-suite/bugs/closed/328.v40
1 files changed, 0 insertions, 40 deletions
diff --git a/test-suite/bugs/closed/328.v b/test-suite/bugs/closed/328.v
deleted file mode 100644
index 52cfbbc4..00000000
--- a/test-suite/bugs/closed/328.v
+++ /dev/null
@@ -1,40 +0,0 @@
-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)).*)