diff options
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 _). |