diff options
author | 2014-09-26 11:22:40 +0200 | |
---|---|---|
committer | 2014-09-26 16:10:13 +0200 | |
commit | dd21327dbc388dfbff88834ae628df062b1b7c04 (patch) | |
tree | 89bf3ebd53126d7861d999889a6d3a526ba3152a /test-suite/bugs/closed/3665.v | |
parent | 0a42f8d2434d6c5471d47c99d815762783cdca95 (diff) |
Fix canonical structure resolution which was launched on the results of
eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
Diffstat (limited to 'test-suite/bugs/closed/3665.v')
-rw-r--r-- | test-suite/bugs/closed/3665.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3665.v b/test-suite/bugs/closed/3665.v new file mode 100644 index 000000000..f6a13596c --- /dev/null +++ b/test-suite/bugs/closed/3665.v @@ -0,0 +1,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. +Variable T0 : Type -> Type. +Variable 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. |