diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/ltac.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 952f35bc35..f9df021dc2 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -304,5 +304,5 @@ Abort. Goal True. let x := ipattern:y in assert (forall x y, x = y + 0). intro. -destruct y. (* Check that the name is y here *). +destruct y. (* Check that the name is y here *) Abort. |