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 ++++++
 parsing/g_tactic.ml4      | 10 ++++++++++
 2 files changed, 16 insertions(+)

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
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 0eab3f7f9c..fe21a876cf 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -204,6 +204,13 @@ GEXTEND Gram
       | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl
     ] ]
   ;
+
+  delta_flag:
+    [ [ IDENT "delta"; "["; idl = LIST1 global; "]" -> FConst idl
+      | IDENT "delta"; "-"; "["; idl = LIST1 global; "]" -> FDeltaBut idl
+    ] ]
+  ;
+
   red_tactic:
     [ [ IDENT "red" -> Red false
       | IDENT "hnf" -> Hnf
@@ -211,6 +218,9 @@ GEXTEND Gram
       | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "compute" -> compute
+      | IDENT "compute"; delta = delta_flag -> 
+	  let s = [FBeta;FIota;FZeta;delta] in 
+	  Cbv (make_red_flag s)
       | IDENT "vm_compute" -> CbvVm
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
-- 
cgit v1.2.3