diff options
| author | Hugo Herbelin | 2014-11-08 10:45:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-08 16:12:03 +0100 |
| commit | c8721369d1d3e6572138fa7aab65e54f68459db4 (patch) | |
| tree | 4e56f6f3f2d5a64a02043dbf796eaec275ac8865 | |
| parent | 7e4241a6aec516b8b28bc0c6f2125c5960b909e7 (diff) | |
Test fixed by PMP's commits from Oct 21.
| -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' _ _ _). |