diff options
Diffstat (limited to 'test-suite/coqdoc/bug5648.v')
| -rw-r--r-- | test-suite/coqdoc/bug5648.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/test-suite/coqdoc/bug5648.v b/test-suite/coqdoc/bug5648.v index 353ecc49a..9b62dd1e1 100644 --- a/test-suite/coqdoc/bug5648.v +++ b/test-suite/coqdoc/bug5648.v @@ -17,8 +17,3 @@ Definition d x := | P => 6 | Proof => 7 end. - -Ltac Next := easy. - -Lemma yes : True. -Proof. Next. Qed. |