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
|
(* File reduced by coq-bug-finder from original input, then from 5449 lines to 44 lines *)
(* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
coqtop version trunk (September 2014) *)
Set Primitive Projections.
Axiom IsHSet : Type -> Type.
Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
Module withdefault.
Canonical Structure default_HSet := fun T P => (@BuildhSet T P).
Goal forall (z : hSet) (T0 : Type -> Type),
(forall (A : Type) (P : T0 A -> Type) (aa : T0 A), P aa) ->
forall x0 : setT z, Set.
clear; intros z T H.
Set Debug Unification.
Fail refine (H _ _). (* Timeout! *)
Abort.
End withdefault.
Module withnondefault.
Parameter T0 : Type -> Type.
Parameter T0hset: forall A, IsHSet (T0 A).
Canonical Structure nondefault_HSet := fun A =>(@BuildhSet (T0 A) (T0hset A)).
Canonical Structure default_HSet := fun A P =>(@BuildhSet A P).
Goal forall (z : hSet) (T0 : Type -> Type),
(forall (A : Type) (P : T0 A -> Type) (aa : T0 A), P aa) ->
forall x0 : setT z, Set.
clear; intros z T H.
Set Debug Unification.
Fail refine (H _ _). (* Timeout! *)
Abort.
End withnondefault.
|
