diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-16 15:56:50 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-16 15:56:50 +0000 |
| commit | 6942f889bfe68b308744a01cc079403e872b4925 (patch) | |
| tree | c1724c4c744b31b7348414ad0418d618a91ffab8 | |
| parent | 22a24e1cadd4e1206db195c9ef19ca3130eb1bc8 (diff) | |
tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8402 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/RefMan.txt | 2 | ||||
| -rw-r--r-- | doc/Reference-Manual.tex | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan.txt b/doc/RefMan.txt index 75a762758..5bbc2e81e 100644 --- a/doc/RefMan.txt +++ b/doc/RefMan.txt @@ -21,7 +21,7 @@ MANUEL DE REFERENCE \part{The proof engine} \include{RefMan-oth.v}% Vernacular commands JCF -fait \include{RefMan-pro}% Proof handling Clement -\include{RefMan-tac.v}% Tactics and tacticals JCF +\include{RefMan-tac.v}% Tactics and tacticals JCF - en cours %% ajouter JProver/Ground/CC Pierre C -fait \include{RefMan-tacex.v}% Detailed Examples of tactics JCF diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index 7a5c5eca4..229fb4524 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-tac.v,RefMan-tacex.v} \input{./version.tex} \input{./macros.tex}% extension .tex pour htmlgen |