From 08e7817810a369d5fd11e7a5f089479b06bd42ad Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 19 Dec 2003 17:25:32 +0000
Subject: deplacement du chap sur ltac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8422 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Reference-Manual.tex | 6 ++----
 1 file 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)
-- 
cgit v1.2.3