From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Fri, 13 Nov 2015 11:31:34 +0100
Subject: Imported Upstream version 8.5~beta3+dfsg

---
 parsing/g_tactic.ml4 | 66 +++++++++++++++++++++++++++++-----------------------
 1 file changed, 37 insertions(+), 29 deletions(-)

(limited to 'parsing/g_tactic.ml4')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 69593f99..c94ac846 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -339,21 +339,6 @@ GEXTEND Gram
       | d = delta_flag -> all_with d
     ] ]
   ;
-  red_tactic:
-    [ [ IDENT "red" -> Red false
-      | IDENT "hnf" -> Hnf
-      | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
-      | IDENT "cbv"; s = strategy_flag -> Cbv s
-      | IDENT "cbn"; s = strategy_flag -> Cbn s
-      | IDENT "lazy"; s = strategy_flag -> Lazy s
-      | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
-      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
-      | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
-      | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
-      | IDENT "fold"; cl = LIST1 constr -> Fold cl
-      | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
-  ;
-  (* This is [red_tactic] including possible extensions *)
   red_expr:
     [ [ IDENT "red" -> Red false
       | IDENT "hnf" -> Hnf
@@ -452,16 +437,6 @@ GEXTEND Gram
     [ [ "using"; l = LIST1 constr SEP "," -> l
       | -> [] ] ]
   ;
-  trivial:
-    [ [ IDENT "trivial" -> Off
-      | IDENT "info_trivial" -> Info
-      | IDENT "debug"; IDENT "trivial" -> Debug ] ]
-  ;
-  auto:
-    [ [ IDENT "auto" -> Off
-      | IDENT "info_auto" -> Info
-      | IDENT "debug"; IDENT "auto" -> Debug ] ]
-  ;
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
@@ -627,9 +602,18 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
       (* Automation tactic *)
-      | d = trivial; lems = auto_using; db = hintbases -> TacAtom (!@loc, TacTrivial (d,lems,db))
-      | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacAuto (d,n,lems,db))
+      | IDENT "trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Off, lems, db))
+      | IDENT "info_trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Info, lems, db))
+      | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Debug, lems, db))
+      | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Off, n, lems, db))
+      | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Info, n, lems, db))
+      | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Debug, n, lems, db))
 
       (* Context management *)
       | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
@@ -677,7 +661,31 @@ GEXTEND Gram
 	    TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
 
       (* Conversion *)
-      | r = red_tactic; cl = clause_dft_concl -> TacAtom (!@loc, TacReduce (r, cl))
+      | IDENT "red"; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Red false, cl))
+      | IDENT "hnf"; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Hnf, cl))
+      | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl))
+      | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbv s, cl))
+      | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbn s, cl))
+      | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Lazy s, cl))
+      | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl))
+      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (CbvVm po, cl))
+      | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (CbvNative po, cl))
+      | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Unfold ul, cl))
+      | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Fold l, cl))
+      | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Pattern pl, cl))
+
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
 	  let p,cl = merge_occurrences (!@loc) cl oc in
-- 
cgit v1.2.3