diff options
Diffstat (limited to 'test-suite')
| -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 1a9e38b79..72973a8d8 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) |