diff options
| author | barras | 2003-12-19 17:25:32 +0000 |
|---|---|---|
| committer | barras | 2003-12-19 17:25:32 +0000 |
| commit | 08e7817810a369d5fd11e7a5f089479b06bd42ad (patch) | |
| tree | 0879fcf46bc38d84db2e1db931c9d2e44c323ef5 /doc | |
| parent | bd4d79c10a1c50334517c0c73e56a40bd1ccefb6 (diff) | |
deplacement du chap sur ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8422 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Reference-Manual.tex | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index 229fb4524b..c20b6d05c6 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -18,7 +18,7 @@ \fi -%\includeonly{RefMan-tac.v,RefMan-tacex.v} +%\includeonly{RefMan-gal.v,RefMan-ltac.v,RefMan-lib.v,Cases.v} \input{./version.tex} \input{./macros.tex}% extension .tex pour htmlgen @@ -43,7 +43,6 @@ \include{RefMan-ext.v}% Gallina extensions \include{RefMan-lib.v}% The coq library \include{RefMan-cic.v}% The Calculus of Constructions - \include{RefMan-modr}% The module system @@ -51,13 +50,12 @@ \include{RefMan-oth.v}% Vernacular commands \include{RefMan-pro}% Proof handling \include{RefMan-tac.v}% Tactics and tacticals +\include{RefMan-ltac.v}% Writing tactics \include{RefMan-tacex.v}% Detailed Examples of tactics \part{User extensions} \include{RefMan-syn.v}% The Syntax and the Grammad commands %%SUPPRIME \include{RefMan-tus.v}% Writing tactics -%%REMPLACE PAR -\include{RefMan-ltac.v}% Writing tactics \part{Practical tools} \include{RefMan-com}% The coq commands (coqc coqtop) |