diff options
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 4736012e8..4380f5442 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -95,8 +95,9 @@ Options A and B of the licence are {\em not} elected.} \include{RefMan-decl.v}% The mathematical proof language \part{User extensions} -\include{RefMan-syn.v}% The Syntax and the Grammad commands +\include{RefMan-syn.v}% The Syntax and the Grammar commands %%SUPPRIME \include{RefMan-tus.v}% Writing tactics +\include{RefMan-sch.v}% The Scheme commands \part{Practical tools} \include{RefMan-com}% The coq commands (coqc coqtop) |