From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Nov 2006 13:20:22 +0000 (+0000)
Subject: The auto parameters that can be given to a declarative rewritingstep must now
X-Git-Tag: 0.4.95@7852~762
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8a219d1957a19d666a929e9a674a5fddee10066b;p=helm.git

The auto parameters that can be given to a declarative rewritingstep must now
be put in parenthesis (to avoid "eating" the "done" token).
---

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 4c1ddffb2..d00f7de7c 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -268,9 +268,9 @@ EXTEND
     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 	 GrafiteAst.Case(loc,id,params)
-    | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params -> `Auto params  ] ; cont=rewriting_step_continuation ->
+    | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params  ] ; cont=rewriting_step_continuation ->
      GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont)
-    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params -> `Auto params ] ;
+    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
       cont=rewriting_step_continuation  ->
      GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
   ]
@@ -281,6 +281,11 @@ EXTEND
        string_of_int v | v = IDENT -> v ] -> i,v ] ->
       params
    ]
+];
+  auto_params': [
+   [ LPAREN; params = auto_params; RPAREN -> params
+   | -> []
+   ]
 ];
   by_continuation: [
     [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)