X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=24d1b3feb441b864d977807b931196e1c3ea33f5;hb=ca2a604c2817deb118d595611b94a0d77978eab6;hp=45a71f174dea678322b79bd97fcaecf0e5a31b79;hpb=73993c770d613df679df63d8d3d89fc37c02ae09;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 45a71f174..24d1b3feb 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -291,11 +291,28 @@ EXTEND
     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 	 GrafiteAst.Case(loc,id,params)
-    | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; 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 (start,termine), t1, t2, cont)
-    | 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)
+    | start =
+       [ IDENT "conclude" -> None
+       | IDENT "obtain" ; name = IDENT -> Some name ] ;
+      termine = tactic_term ;
+      SYMBOL "=" ;
+      t1=tactic_term ;
+      IDENT "by" ;
+      t2 =
+       [ t=tactic_term -> `Term t
+       | SYMBOL "_" ; params = auto_params' -> `Auto params
+       | IDENT "proof" -> `Proof] ;
+      cont = rewriting_step_continuation ->
+       GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
+    | SYMBOL "=" ;
+      t1=tactic_term ;
+      IDENT "by" ;
+      t2=
+       [ t=tactic_term -> `Term t
+       | SYMBOL "_" ; params = auto_params' -> `Auto params
+       | IDENT "proof" -> `Proof] ;
+      cont=rewriting_step_continuation ->
+       GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
   ]
 ];
   auto_params: [