diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 21:08:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 21:45:48 +0200 |
| commit | 97fba91264669d495643f6a3de6a09790ae2a1da (patch) | |
| tree | 713f13b9c63763d20e1984e594abb449530984df /test-suite/success/ltac.v | |
| parent | 47b4573a77ef88f8528c8247108eba8b04d81525 (diff) | |
Continuing 817308ab (use ltac env for terms in ltac context) + fix
of syntax in test file ltac.v.
Diffstat (limited to 'test-suite/success/ltac.v')
| -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 952f35bc3..f9df021dc 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. |