diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-15 17:10:37 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-15 17:10:37 +0000 |
| commit | 730e25488e0f502359ed8c2a845b97bf0245d1e7 (patch) | |
| tree | d81f83c5c825e865ceb4fda85482e609bcebb58b /doc/refman/Reference-Manual.tex | |
| parent | 92616b9f660eaa2640964ca1925b05d37af70c8c (diff) | |
Port rewrites of tactic documentation from branch 8.4.
This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277,
r15278, r15337. The merge did not go without troubles, but hopefully none
of the changes were lost in process.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7
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) |