diff options
| -rw-r--r-- | doc/RefMan.txt | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan.txt b/doc/RefMan.txt index 752462670e..3c3d88ba8e 100644 --- a/doc/RefMan.txt +++ b/doc/RefMan.txt @@ -34,7 +34,7 @@ MANUEL DE REFERENCE \part{Practical tools} \include{RefMan-com}% The coq commands (coqc coqtop) HH %%ajouter nouvelles options -v7 -translate au document de passage -\include{RefMan-uti}% utilities (gallina, do_Makefile, etc) JCF +\include{RefMan-uti}% utilities (gallina, do_Makefile, etc) JCF -fait \include{RefMan-ide}%CoqIde CM \include{AddRefMan-pre}% CP |