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 | |
parent | f5a096a0f9c628f944a6d57a939c6819d04001c3 (diff) |
Fix test-suite scripts.
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/3618.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/3710.v | 4 |
2 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/3618.v b/test-suite/bugs/closed/3618.v index bbce32e9e..dc560ad52 100644 --- a/test-suite/bugs/closed/3618.v +++ b/test-suite/bugs/closed/3618.v @@ -98,6 +98,6 @@ Admitted. (* To avoid looping class resolution *) Hint Mode IsEquiv - - + : typeclass_instances. -Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse} +Fail Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse} (P Q : Type) {Q_inO : inO_internal Q} : IsEquiv (fun f : O P -> P => compose f (O_unit P)) := _.
\ No newline at end of file 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 _). |