From 471df7db322e77a3cb66a8def53c7ddfdb9c8769 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Nov 2007 10:40:23 +0000
Subject: Suite ajout raccourcis à compute et lazy pour réduire tout sauf
 certaines constantes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10310 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 33 ++++++++++++++++-----------------
 1 file changed, 16 insertions(+), 17 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e8d1be4f63..9b21837d8b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -18,7 +18,7 @@ open Rawterm
 open Genarg
 open Topconstr
 
-let compute = Cbv all_flags
+let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
 
 let tactic_kw = [ "->"; "<-" ]
 let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
@@ -212,30 +212,29 @@ GEXTEND Gram
   ;
   red_flag:
     [ [ IDENT "beta" -> FBeta
-      | IDENT "delta" -> FDeltaBut []
       | IDENT "iota" -> FIota
       | IDENT "zeta" -> FZeta
-      | IDENT "delta"; "["; idl = LIST1 smart_global; "]" -> FConst idl
-      | IDENT "delta"; "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl
+      | IDENT "delta"; d = delta_flag -> d
     ] ]
   ;
-
   delta_flag:
-    [ [ IDENT "delta"; "["; idl = LIST1 smart_global; "]" -> FConst idl
-      | IDENT "delta"; "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl
+    [ [ "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl
+      | "["; idl = LIST1 smart_global; "]" -> FConst idl
+      | -> FDeltaBut []
+    ] ]
+  ;
+  strategy_flag:
+    [ [ s = LIST1 red_flag -> make_red_flag s
+      | d = delta_flag -> all_with d
     ] ]
   ;
-
   red_tactic:
     [ [ IDENT "red" -> Red false
       | IDENT "hnf" -> Hnf
       | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
-      | 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 "cbv"; s = strategy_flag -> Cbv s
+      | IDENT "lazy"; s = strategy_flag -> Lazy s
+      | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
       | IDENT "vm_compute" -> CbvVm
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
@@ -246,9 +245,9 @@ GEXTEND Gram
     [ [ IDENT "red" -> Red false
       | IDENT "hnf" -> Hnf
       | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
-      | 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 "cbv"; s = strategy_flag -> Cbv s
+      | IDENT "lazy"; s = strategy_flag -> Lazy s
+      | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
       | IDENT "vm_compute" -> CbvVm
       | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
-- 
cgit v1.2.3