aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-27 21:10:30 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-27 21:10:30 +0100
commit78d1a61730886f89b01fa4245e58b54dd50fb4cf (patch)
treee142dc038bca551d4a6ef947c1432b757dba90c7 /test-suite
parentfc1b3ef9d7270938cd83c524aae0383093b7a4b5 (diff)
Adding a test for bug #3612.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/3612.v47
1 files changed, 47 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
new file mode 100644
index 000000000..9125ab16d
--- /dev/null
+++ b/test-suite/bugs/closed/3612.v
@@ -0,0 +1,47 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 3595 lines to 3518 lines, then from 3133 lines to 2950 lines, then from 2911 lines to 415 lines, then from 431 lines to 407 \
+lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then from 434 lines to 66 lines, then from 163 lines to 48 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 11 2014 14:48:8 with OCaml 4.01.0
+ coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (580b25e05c7cc9e7a31430b3d9edb14ae12b7598) *)
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "x = y :> T" (at level 70, y at next level, no associativity).
+Reserved Notation "x = y" (at level 70, no associativity).
+Open Scope type_scope.
+Global Set Universe Polymorphism.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Generalizable All Variables.
+Local Set Primitive Projections.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} _ / .
+Arguments projT2 {A P} _ / .
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y .
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+Local Open Scope path_scope.
+Axiom pr1_path : forall `{P : A -> Type} {u v : sigT P} (p : u = v), u.1 = v.1.
+Notation "p ..1" := (pr1_path p) (at level 3) : fibration_scope.
+Axiom pr2_path : forall `{P : A -> Type} {u v : sigT P} (p : u = v), p..1 # u.2 = v.2.
+Notation "p ..2" := (pr2_path p) (at level 3) : fibration_scope.
+Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
+ (p q : u = v)
+ (r : p..1 = q..1)
+ (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
+p = q.
+Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
+ (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
+ @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
+ (@idpath (@sigT A (fun x0 : A => B x0)) x).
+ intros A B x xx.
+ Set Printing All.
+ change (fun x => B x) with B in xx.
+ pose (path_path_sigma B x x xx) as x''.
+ clear x''.
+ Check (path_path_sigma B x x xx).