From a1cf9fb6d588b706d298857f2bc6bb1a9229db19 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 5 Apr 2001 12:37:02 +0000
Subject: ajout chapitre langage de tactiques; suppression chapitre obsoletes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8163 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Extraction.tex       | 9 +++++----
 doc/RefMan-ltac.tex      | 4 ++++
 doc/Reference-Manual.tex | 8 +++++---
 3 files changed, 14 insertions(+), 7 deletions(-)
 create mode 100644 doc/RefMan-ltac.tex

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 45f7b81e57..53c6bec24c 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -549,9 +549,10 @@ remains balanced:
 
 \section{Bugs}
 
-Surely there are still bugs in the {\tt Extraction} module.
-You can send your bug reports directly to the author
-(at \textsf{Jean-Christophe.Filliatre$@$lri.fr}) or to the \Coq\
-mailing list (at \textsf{coq$@$pauillac.inria.fr}).
+Surely there are still bugs in the {\tt Extraction} module.  You can
+send your bug reports directly to the authors
+(\textsf{Pierre.Letouzey$@$lri.fr} and
+\textsf{Jean-Christophe.Filliatre$@$lri.fr}) or to the \Coq\ mailing
+list (at \textsf{coq$@$pauillac.inria.fr}).
 
 % $Id$ 
diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
new file mode 100644
index 0000000000..c2ee955a61
--- /dev/null
+++ b/doc/RefMan-ltac.tex
@@ -0,0 +1,4 @@
+\chapter{The tactic language}
+\label{WritingTactics}
+
+**TO DO**
\ No newline at end of file
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 4677e1ab67..cdcf3274fa 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -44,7 +44,9 @@
 
 \part{User extensions}
 \include{RefMan-syn.v}% The Syntax and the Grammad commands
-\include{RefMan-tus.v}% Writing tactics
+%%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)
@@ -53,9 +55,9 @@
 \include{AddRefMan-pre}%
 \include{Cases.v}%
 \include{Coercion.v}%
-\include{Natural.v}%
+%%SUPPRIME \include{Natural.v}%
 \include{Omega.v}%
-\include{Program.v}%
+%%SUPPRIME \include{Program.v}%
 \include{Programs.v}% = preuve de pgms imperatifs
 \include{Extraction.v}%
 \include{Polynom.v}%  = Ring
-- 
cgit v1.2.3