diff options
author | 2016-01-12 20:49:34 +0100 | |
---|---|---|
committer | 2016-01-12 22:17:45 +0100 | |
commit | be4bfc78c493464cb0af40d7fae08ba86295a6f9 (patch) | |
tree | dca0b2628e1ddfa0f64cf66234c225399a43f728 /test-suite/bugs/closed/4256.v | |
parent | 74d89e0be05e5cb4c9faf154478bc0c907bec2bb (diff) |
Fixing #4256 and #4484 (changes in evar-evar resolution made that new
evars were created making in turn that evars formerly recognized as
pending were not anymore in the list of pending evars). This also
fixes the reopening of #3848.
See comments on #4484 for details.
Diffstat (limited to 'test-suite/bugs/closed/4256.v')
-rw-r--r-- | test-suite/bugs/closed/4256.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v new file mode 100644 index 000000000..3cdc4ada0 --- /dev/null +++ b/test-suite/bugs/closed/4256.v @@ -0,0 +1,43 @@ +(* Testing 8.5 regression with type classes not solving evars + redefined while trying to solve them with the type class mechanism *) + +Global Set Universe Polymorphism. +Monomorphic Universe i. +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. +Notation "-1" := (trunc_S minus_two) (at level 0). + +Class IsPointed (A : Type) := point : A. +Arguments point A {_}. + +Record pType := + { pointed_type : Type ; + ispointed_type : IsPointed pointed_type }. +Coercion pointed_type : pType >-> Sortclass. +Existing Instance ispointed_type. + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + + + +Record ooGroup := + { classifying_space : pType@{i} }. + +Definition group_loops (X : pType) +: ooGroup. +Proof. + (** This works: *) + pose (x0 := point X). + pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)). + clear H x0. + (** But this doesn't: *) + pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)). |