From 03fc5f1d7c143ef65cfc7258e5e158d8405f05a1 Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 1 Sep 2006 08:08:22 +0000
Subject: Modification du manuel de référence: le flag evar pour cbv n'existe
 plus.

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

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1dd534ca29..10e32675b1 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -774,9 +774,7 @@ followed by {\tt [\qualid$_1$\ldots\qualid$_k$]} or {\tt
   -[\qualid$_1$\ldots\qualid$_k$]}), the {\tt delta} flag means that all constants must be unfolded.
 However, the {\tt delta} flag does not apply to variables bound by a
 let-in construction whose unfolding is controlled by the {\tt
-  zeta} flag only.  In addition, there is a flag {\tt Evar} to perform
-instantiation of existential variables (``?'') when an instantiation
-actually exists. 
+  zeta} flag only.
 
 The goal may be normalized with two strategies: {\em lazy} ({\tt lazy}
 tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy
@@ -799,7 +797,7 @@ computational expressions (i.e. with few dead code).
 \begin{Variants}
 \item {\tt compute} \tacindex{compute} 
   
-  This tactic is an alias for {\tt cbv beta delta evar iota zeta}.
+  This tactic is an alias for {\tt cbv beta delta iota zeta}.
 
 \item {\tt vm\_compute} \tacindex{vm\_compute}
 
-- 
cgit v1.2.3