From 1b09098cc4830f262820d2935a9cd0afa383ed3f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 1 Jul 2016 13:57:14 +0200
Subject: Add and document match, fix and cofix reduction flags.

---
 parsing/g_tactic.ml4 | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8a83bc2d1d..33ca9158cd 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -22,7 +22,7 @@ open Decl_kinds
 open Pcoq
 
 
-let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta]
+let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
 
 let tactic_kw = [ "->"; "<-" ; "by" ]
 let _ = List.iter CLexer.add_keyword tactic_kw
@@ -348,11 +348,14 @@ GEXTEND Gram
   with_bindings:
     [ [ "with"; bl = bindings -> bl | -> NoBindings ] ]
   ;
-  red_flag:
-    [ [ IDENT "beta" -> FBeta
-      | IDENT "iota" -> FIota
-      | IDENT "zeta" -> FZeta
-      | IDENT "delta"; d = delta_flag -> d
+  red_flags:
+    [ [ IDENT "beta" -> [FBeta]
+      | IDENT "iota" -> [FMatch;FFix;FCofix]
+      | IDENT "match" -> [FMatch]
+      | IDENT "fix" -> [FFix]
+      | IDENT "cofix" -> [FCofix]
+      | IDENT "zeta" -> [FZeta]
+      | IDENT "delta"; d = delta_flag -> [d]
     ] ]
   ;
   delta_flag:
@@ -362,7 +365,7 @@ GEXTEND Gram
     ] ]
   ;
   strategy_flag:
-    [ [ s = LIST1 red_flag -> Redops.make_red_flag s
+    [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s)
       | d = delta_flag -> all_with d
     ] ]
   ;
-- 
cgit v1.2.3