blob: e69ec1097692eecd9e94407e7eef55a8635a013e (
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
39
40
41
42
43
44
45
46
47
48
49
50
51
|
Unset Strict Universe Declaration.
(* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *)
(* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
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).
Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V.
Module NonPrim.
Record hProp := hp { hproptype :> Type ; isp : Set}.
Goal forall (A B : Type) (H_f : A -> V -> hProp) (H_g : B -> V -> hProp)
(C : Type) (h : C -> V) (b : B) (a : A) (c : C),
H_f a (h c) -> H_f a (h c) = H_g b (h c) -> H_g b (h c).
intros A B H_f H_g C h b a c H3 H'.
exact (@transport hProp (fun x => x) _ _ H' H3).
Undo.
Set Debug Unification.
exact (H' # H3).
Defined.
End NonPrim.
Module Prim.
Set Primitive Projections.
Set Universe Polymorphism.
Record hProp := hp { hproptype :> Type ; isp : Set}.
Goal forall (A B : Type) (H_f : A -> V -> hProp) (H_g : B -> V -> hProp)
(C : Type) (h : C -> V) (b : B) (a : A) (c : C),
H_f a (h c) -> H_f a (h c) = H_g b (h c) -> H_g b (h c).
intros A B H_f H_g C h b a c H3 H'.
exact (@transport hProp (fun x => x) _ _ H' H3).
Undo.
Set Debug Unification.
exact (H' # H3).
(* Toplevel input, characters 7-14:
Error:
In environment
A : Type
B : Type
H_f : A -> V -> hProp
H_g : B -> V -> hProp
C : Type
h : C -> V
b : B
a : A
c : C
H3 : H_f a (h c)
H' : H_f a (h c) = H_g b (h c)
Unable to unify "hproptype (H_f a (h c))" with "?T (H_f a (h c))".
*)
Defined.
End Prim.
|
