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 4c1ddffb20c07617f96b4da6fbb3340aa8b2ceb4..d00f7de7cfa065215969c7e49e55f7ccc989b20f 100644 (file)
--- 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)