diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/3665.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
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 00000000..f6a13596 --- /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. |