From: Claudio Sacerdoti Coen 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)