From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/3428.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 test-suite/bugs/closed/3428.v (limited to 'test-suite/bugs/closed/3428.v') diff --git a/test-suite/bugs/closed/3428.v b/test-suite/bugs/closed/3428.v new file mode 100644 index 00000000..3eb75e43 --- /dev/null +++ b/test-suite/bugs/closed/3428.v @@ -0,0 +1,35 @@ +(* File reduced by coq-bug-finder from original input, then from 2809 lines to 39 lines *) +Set Primitive Projections. +Set Implicit Arguments. +Module Export foo. + Record prod (A B : Type) := pair { fst : A ; snd : B }. +End foo. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Arguments idpath {A a} , [A] a. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. +Axiom path_prod : forall {A B : Type} (z z' : prod A B), (fst z = fst z') -> (snd z = snd z') -> (z = z'). +Notation fst := (@fst _ _). +Notation snd := (@snd _ _). +Definition ap_fst_path_prod {A B : Type} {z z' : prod A B} (p : @paths A (fst z) (fst z')) (q : snd z = snd z') +: ap fst (path_prod z z' p q) = p. +Abort. + +Notation fstp x := (x.(foo.fst)). +Notation fstap x := (foo.fst x). + +Definition ap_fst_path_prod' {A B : Type} {z z' : prod A B} (p : @paths A (fst z) (fst z')) (q : snd z = snd z') +: ap (fun x => fstap x) (path_prod z z' p q) = p. + +Abort. + +(* Toplevel input, characters 137-138: +Error: +In environment +A : Type +B : Type +z : prod A B +z' : prod A B +p : @paths A (foo.fst ?11 ?14 z) (foo.fst ?26 ?29 z') +q : @paths ?54 (foo.snd ?42 ?45 z) (foo.snd ?57 ?60 z') +The term "p" has type "@paths A (foo.fst ?11 ?14 z) (foo.fst ?26 ?29 z')" +while it is expected to have type "@paths A (foo.fst z) (foo.fst z')". *) \ No newline at end of file -- cgit v1.2.3