Non parenthesage des applications de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1590 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 38 insertions, 3 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 709cc10306..ff4a0a7580 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -43,8 +43,8 @@ GEXTEND Gram
   ;
   constr:
     [ [ c = constr8 -> c 
-      | IDENT "Context"; id = ident; IDENT "With"; c = constr8 ->
-        <:ast< (CONTEXT $id $c) >>
+(*      | IDENT "Context"; id = ident; IDENT "With"; c = constr8 ->
+        <:ast< (CONTEXT $id $c) >>*)
       | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 ->
         <:ast< (EVAL $c (REDEXP $rtc)) >> ] ]
   ;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 6a4ee990d0..205026ed68 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -281,7 +281,14 @@ GEXTEND Gram
          <:ast< (TACTICLIST $ta0 $ta1) >>
       | ta = tactic_expr; ";"; "["; lta = LIST0 tactic_expr SEP "|"; "]" ->
          <:ast< (TACTICLIST $ta (TACLIST ($LIST $lta))) >>
-      | y = tactic_atom -> y ] ]
+      | y = tactic_atom0 -> y ] ]
+  ;
+  tactic_atom0:
+    [ [ la = LIST1 tactic_atom ->
+        if (List.length la) = 1 then
+          let el = List.hd la in <:ast< $el >>
+        else
+          <:ast< (APP ($LIST $la)) >> ] ]
   ;
   tactic_atom:
     [ [ IDENT "Fun"; it = LIST1 input_fun ; "->"; body = tactic_expr ->
@@ -310,6 +317,30 @@ GEXTEND Gram
         -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
       |	IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list ->
         <:ast< (MATCH $com ($LIST $mrl)) >>
+
+(*      | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+          <:ast<(FIRST ($LIST $l))>>
+      |	IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+          <:ast<(TCLSOLVE ($LIST $l))>>
+      | IDENT "Info"; tc = tactic_expr_par -> <:ast< (INFO $tc) >>
+      |	IDENT "Try"; ta0 = tactic_expr_par; "Orelse"; ta1 = tactic_expr_par ->
+        <:ast< (TRY (ORELSE $ta0 $ta1)) >>
+      |	IDENT "Try"; ta = tactic_expr_par -> <:ast< (TRY $ta) >>
+      | IDENT "Do"; n = pure_numarg; ta = tactic_expr_par ->
+        <:ast< (DO $n $ta) >>
+      | IDENT "Repeat"; ta = tactic_expr_par -> <:ast< (REPEAT $ta) >>
+      |	IDENT "Repeat"; ta0 = tactic_expr_par; "Orelse";
+        ta1 = tactic_expr_par ->
+        <:ast< (REPEAT (ORELSE $ta0 $ta1)) >>
+      |	IDENT "Idtac" -> <:ast< (IDTAC) >>
+      |	IDENT "Fail" -> <:ast<(FAIL)>>
+      |	IDENT "Fail"; n = pure_numarg -> <:ast<(FAIL $n)>>
+      |	st = simple_tactic -> st
+      |	st = simple_tactic; "Orelse"; ta1 = tactic_expr_par ->
+          <:ast< (ORELSE $st $ta1) >>
+      |	ta0 = tactic_expr_par; "Orelse"; ta1 = tactic_expr_par ->
+          <:ast< (ORELSE $ta0 $ta1) >>*)
+
       |	"("; te = tactic_expr; ")" -> te
       |	"("; te = tactic_expr; tel=LIST1 tactic_expr; ")" ->
         <:ast< (APP $te ($LIST tel)) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index a5af0845b6..7cbc4d5d7a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -327,8 +327,10 @@ module Tactic =
     let simple_tactic = gec "simple_tactic"
     let tactic = gec "tactic"
     let tactic_arg = gec "tactic_arg"
+    let tactic_atom0 = gec "tactic_atom0"
     let tactic_atom = gec "tactic_atom"
     let tactic_expr = gec "tactic_expr"
+    let tactic_expr_par = gec "tactic_expr_par"
     let unfold_occ = gec "unfold_occ"
     let with_binding_list = gec "with_binding_list"
     let fixdecl = gec_list "fixdecl"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 20bf35dea4..fda1c94cb2 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -152,9 +152,11 @@ module Tactic :
     val simple_tactic : Coqast.t Gram.Entry.e
     val tactic : Coqast.t Gram.Entry.e
     val tactic_arg : Coqast.t Gram.Entry.e
+    val tactic_atom0 : Coqast.t Gram.Entry.e
     val tactic_atom : Coqast.t Gram.Entry.e
     val tactic_eoi : Coqast.t Gram.Entry.e
     val tactic_expr : Coqast.t Gram.Entry.e
+    val tactic_expr_par : Coqast.t Gram.Entry.e
     val unfold_occ : Coqast.t Gram.Entry.e
     val with_binding_list : Coqast.t Gram.Entry.e
   end