diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-10-16 17:30:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-10-16 17:30:42 +0200 |
| commit | 1f7fd3c91d41d661587c90f10cacba4728f38dfc (patch) | |
| tree | 05448cbf75901f84240b6bfd3ae782cf986b1dec /test-suite/bugs/closed/3710.v | |
| parent | f5a096a0f9c628f944a6d57a939c6819d04001c3 (diff) | |
Fix test-suite scripts.
Diffstat (limited to 'test-suite/bugs/closed/3710.v')
| -rw-r--r-- | test-suite/bugs/closed/3710.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/3710.v b/test-suite/bugs/closed/3710.v index 867e31ddf..b9e2798d8 100644 --- a/test-suite/bugs/closed/3710.v +++ b/test-suite/bugs/closed/3710.v @@ -45,6 +45,4 @@ Context `{P : PreCategory -> Type}. Local Notation cat := (@sub_pre_cat P). Goal forall (s d d' : cat) (m1 : morphism cat d d') (m2 : morphism cat s d), NaturalIsomorphism (m1 o m2) (m1 o m2)%functor. - exact (fun _ _ _ _ _ => reflexivity _). -(* Toplevel input, characters 15-54: -Anomaly: variable o unbound. Please report. *)
\ No newline at end of file +Fail exact (fun _ _ _ _ _ => reflexivity _). |