diff options
Diffstat (limited to 'doc/RefMan-int.tex')
| -rwxr-xr-x | doc/RefMan-int.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex index 83a7a90777..9671c99177 100755 --- a/doc/RefMan-int.tex +++ b/doc/RefMan-int.tex @@ -71,7 +71,7 @@ below. \item The third part describes how to extend the system in two ways: adding parsing and pretty-printing rules (chapter \ref{Addoc-syntax}) and writing new tactics (chapter - \ref{WritingTactics}) + \ref{TacticLanguage}) \item In the fourth part more practical tools are documented. First in |