From be4bfc78c493464cb0af40d7fae08ba86295a6f9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Jan 2016 20:49:34 +0100 Subject: 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. --- test-suite/bugs/opened/3848.v | 22 ---------------------- 1 file changed, 22 deletions(-) delete mode 100644 test-suite/bugs/opened/3848.v (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v deleted file mode 100644 index a03e8ffda..000000000 --- a/test-suite/bugs/opened/3848.v +++ /dev/null @@ -1,22 +0,0 @@ -Require Import TestSuite.admit. -Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. -Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing). -Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x. -Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }. -Arguments eisretr {A B} f {_} _. -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'"). -Generalizable Variables A B f g e n. -Definition functor_forall `{P : A -> Type} `{Q : B -> Type} - (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b) -: (forall a:A, P a) -> (forall b:B, Q b). - admit. -Defined. - -Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type} - `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)} -: (forall b : B, Q b) -> forall a : A, P a. -Proof. - refine (functor_forall - (f^-1) - (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)). -Fail Defined. (* Error: Attempt to save an incomplete proof *) -- cgit v1.2.3