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

2 files changed, 21 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index 2d36f32ada..c0fe42112e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,11 @@ Commands
   automatically computed (e.g. Scheme Induction for nat Sort Set).
 - Source of universe inconsistencies now printed when option 
   "Set Printing Universes" is activated,
+- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the "compute" 
+  reduction strategy, respectively meaning reduce only, or everything
+  but, the constants id1 ... idn. "lazy" alone or followed by
+  "[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply
+  all of beta-iota-zeta-delta, possibly restricting delta.
 
 Libraries
 
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