diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1643.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1643.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v index 4114987d..879a65b1 100644 --- a/test-suite/bugs/closed/shouldsucceed/1643.v +++ b/test-suite/bugs/closed/shouldsucceed/1643.v @@ -10,7 +10,6 @@ Definition decomp_func (s:Str) := Theorem decomp s: s = decomp_func s. Proof. - intros s. case s; simpl; reflexivity. Qed. |