diff options
| author | Hugo Herbelin | 2015-08-02 21:08:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 21:45:48 +0200 |
| commit | 97fba91264669d495643f6a3de6a09790ae2a1da (patch) | |
| tree | 713f13b9c63763d20e1984e594abb449530984df /doc/tutorial/Tutorial.tex | |
| parent | 47b4573a77ef88f8528c8247108eba8b04d81525 (diff) | |
Continuing 817308ab (use ltac env for terms in ltac context) + fix
of syntax in test file ltac.v.
Diffstat (limited to 'doc/tutorial/Tutorial.tex')
0 files changed, 0 insertions, 0 deletions