From 2b35ffb42735b9e3af78b06a01d18610fb1f3f97 Mon Sep 17 00:00:00 2001
From: jnarboux
Date: Fri, 9 Jun 2006 16:29:01 +0000
Subject: ajout de la doc de classical_right et left

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8938 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1663b975ab..4946be8f22 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2108,6 +2108,17 @@ datatype: see~\ref{quote-examples} for the full details.
 % En attente d'un moyen de valoriser les fichiers de demos
 % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution
 
+\section{Classical tactics}
+\label{ClassicalTactics}
+
+In order to ease the proving process, when the {\tt Classical} module is loaded. A few more tactics are available. Make sure to load the module using the \texttt{Require Import} command.
+
+\subsection{{\tt classical\_left, classical\_right} \tacindex{classical\_left} \tacindex{classical\_right}}
+
+The tactics \texttt{classical\_left} and \texttt{classical\_right} are the analog of the \texttt{left} and \texttt{right} but using classical logic. They can only be used for disjunctions.
+Use  \texttt{classical\_left} to prove the left part of the disjunction with the assumption that the negation of right part holds. 
+Use \texttt{classical\_left} to prove the right part of the disjunction with the assumption that the negation of left part holds. 
+
 \section{Automatizing
 \label{Automatizing}}
 
-- 
cgit v1.2.3