diff options
| -rw-r--r-- | test-suite/bugs/closed/3258.v (renamed from test-suite/bugs/opened/3258.v) | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/3258.v b/test-suite/bugs/closed/3258.v index 69a543044b..a1390e3025 100644 --- a/test-suite/bugs/opened/3258.v +++ b/test-suite/bugs/closed/3258.v @@ -13,7 +13,6 @@ Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop. Global Instance refine_PreOrder A : PreOrder (@refine A). Admitted. - Add Parametric Morphism A : (@Pick A) with signature @@ -32,4 +31,5 @@ Proof. intros. setoid_rewrite (@remove_forall_eq' _ _ _ _). Undo. - Fail setoid_rewrite (@remove_forall_eq' _ _ _). + (* This failed with NotConvertible at some time *) + setoid_rewrite (@remove_forall_eq' _ _ _). |