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/opened/3848.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/opened/3848.v')
-rw-r--r-- | test-suite/bugs/opened/3848.v | 22 |
1 files changed, 0 insertions, 22 deletions
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 *) |