From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- test-suite/bugs/closed/4256.v | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 test-suite/bugs/closed/4256.v (limited to 'test-suite/bugs/closed/4256.v') diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v new file mode 100644 index 00000000..3cdc4ada --- /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)). -- cgit v1.2.3