New syntax and semantics for the rewriting steps that make the pretty-printed

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index d00f7de7cfa065215969c7e49e55f7ccc989b20f..fb0128edb0ceb63c423c53832d4eedb1681dd24a 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -268,8 +268,8 @@ 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 ->
-     GrafiteAst.RewritingStep(loc, Some termine, 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  ] ; 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)
@@ -299,9 +299,8 @@ EXTEND
     ]
 ];
   rewriting_step_continuation : [
-    [ IDENT "done" -> None
-    | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
-    | -> Some Cic.Anonymous
+    [ IDENT "done" -> true
+    | -> false
     ]
 ];
   atomic_tactical: