diff options
| author | herbelin | 2003-12-20 10:50:53 +0000 |
|---|---|---|
| committer | herbelin | 2003-12-20 10:50:53 +0000 |
| commit | 73b1a1971fd777b7d551d22cdf3f10fbe0711826 (patch) | |
| tree | db3bfb9922bd2fb4a2ea2db45580b9baebb05b3b | |
| parent | ac54e608ff496efb281c68a07eea0f48f2fb6859 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8431 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/RefMan.txt | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/RefMan.txt b/doc/RefMan.txt index 61f05cc13f..44422c792e 100644 --- a/doc/RefMan.txt +++ b/doc/RefMan.txt @@ -11,7 +11,7 @@ MANUEL DE REFERENCE \part{The language} \defaultheaders \include{RefMan-gal.v}% Gallina BB -\include{RefMan-ext.v}% Gallina extensions HH +\include{RefMan-ext.v}% Gallina extensions HH -fait \include{RefMan-lib.v}% The coq library BB \include{RefMan-cic.v}% The Calculus of Constructions CP @@ -32,7 +32,7 @@ MANUEL DE REFERENCE \include{RefMan-ltac.v}% Writing tactics BB -fait \part{Practical tools} -\include{RefMan-com}% The coq commands (coqc coqtop) HH +\include{RefMan-com}% The coq commands (coqc coqtop) HH -fait %%ajouter nouvelles options -v7 -translate au document de passage \include{RefMan-uti}% utilities (gallina, do_Makefile, etc) JCF -fait \include{RefMan-ide}%CoqIde CM @@ -40,7 +40,7 @@ MANUEL DE REFERENCE \include{AddRefMan-pre}% CP \include{Cases.v}% CP -\include{Coercion.v}% HH +\include{Coercion.v}% HH -fait %%SUPPRIME \include{Natural.v}% \include{Omega.v}% JCF - fait %%Nouvelle version ROmega Pierre Cregut |