diff options
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/3417.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/3417.v b/test-suite/bugs/opened/3417.v deleted file mode 100644 index 355fd17ff9..0000000000 --- a/test-suite/bugs/opened/3417.v +++ /dev/null @@ -1,3 +0,0 @@ -Goal forall {T}(a b : T), b=a -> {c | c=b}. -intros T a b H. -Fail setoid_rewrite H. |