diff options
| author | Matthieu Sozeau | 2014-10-15 13:53:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-15 13:53:42 +0200 |
| commit | 9d66b52dee17dcbdb45522fe3fcfa1fcdae65862 (patch) | |
| tree | 21a0d9ab87b3f6436f5d3ef552b208d6b0920ee9 | |
| parent | 5467fc3ee8249d5e1978cba5006db98cdfc27384 (diff) | |
Bug 3692 is fixed.
| -rw-r--r-- | test-suite/bugs/closed/3692.v (renamed from test-suite/bugs/opened/3692.v) | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3692.v b/test-suite/bugs/closed/3692.v index 1a9e38b794..72973a8d81 100644 --- a/test-suite/bugs/opened/3692.v +++ b/test-suite/bugs/closed/3692.v @@ -19,7 +19,7 @@ Definition functor_prod {A A' B B' : Type} (f:A->A') (g:B->B') : A * B -> A' * B'. exact (fun z => (f (fst z), g (snd z))). Defined. -Fail Definition isequiv_functor_prod `{IsEquiv A A' f} `{IsEquiv B B' g} +Definition isequiv_functor_prod `{IsEquiv A A' f} `{IsEquiv B B' g} : IsEquiv (functor_prod f g) := @Build_IsEquiv _ _ (functor_prod f g) (functor_prod f^-1 g^-1) |