blob: 679721667ad192160f9b15bd48a9d09211c6f3ae (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
(* File reduced by coq-bug-finder from original input, then from 11716 lines to 11295 lines, then from 10518 lines to 21 lines, then \
from 37 lines to 21 lines *)
(* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml 4.01.0
coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *)
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.
Arguments pair {A B} _ _.
Arguments fst {A B} _ / .
Arguments snd {A B} _ / .
Notation "x * y" := (prod x y) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> H * H0)
(H4 : (fun c : H1 => (fst (H3 c), snd (H3 c))%core) =
H3) (H5 : H -> Type) (H6 H7 : H5 (fst (H3 H2))),
transport (fun y : H1 -> H * H0 => H5 (fst (y H2))) H4 H6 = H7.
intros.
match goal with
| [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ]
=> set(foo:=h); idtac
end.
match goal with
| [ |- appcontext ctx [transport (fun y => (?g (fst (y H2))))] ]
=> idtac
end.
Abort.
Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> (H1 -> H) * H0)
(H4 : (fun c : H1 => (fst (H3 c), snd (H3 c))%core) =
H3) (H5 : H -> Type) (H6 H7 : H5 (fst (H3 H2) H2)),
transport (fun y : H1 -> (H1 -> H) * H0 => H5 (fst (y H2) H2)) H4 H6 = H7.
intros.
match goal with
| [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ]
=> set(foo:=X)
end.
(* Anomaly: Uncaught exception Not_found(_). Please report. *)
(* Anomaly: Uncaught exception Not_found(_). Please report. *)
|
