1. "by proof" now allowed as a justification in equality chains.

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 45a71f174dea678322b79bd97fcaecf0e5a31b79..24d1b3feb441b864d977807b931196e1c3ea33f5 100644 (file)
--- 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: [