From 548fd57a9910a1622348c4a6f6f44f8d8a262bb1 Mon Sep 17 00:00:00 2001
From: jforest
Date: Thu, 5 Apr 2007 16:53:46 +0000
Subject: Mise en place d'un rafinement de compute. On peut desormais utiliser:
 compute delta [f g ...] pour cbv beta iota zera delta [f g ...] et compute
 delta - [f g ...] pour cbv beta iota zera delta - [f g ...]

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d2753371b8..8331defbb5 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -873,6 +873,12 @@ computational expressions (i.e. with few dead code).
   
   This tactic is an alias for {\tt cbv beta delta iota zeta}.
 
+\item {\tt compute delta [\qualid$_1$\ldots\qualid$_k$]} (resp. {\tt compute delta  -[\qualid$_1$\ldots\qualid$_k$]})  \tacindex{compute} 
+
+      This tactic is an alias for {\tt cbv beta delta iota zeta [\qualid$_1$\ldots\qualid$_k$]} (resp. {\tt cbv beta delta iota zeta -[\qualid$_1$\ldots\qualid$_k$]}) .
+  
+  This tactic is an alias for {\tt cbv beta delta iota zeta}.
+
 \item {\tt vm\_compute} \tacindex{vm\_compute}
 
   This tactic evaluates the goal using the optimized call-by-value
-- 
cgit v1.2.3