"that is equivalent to" and "or equivalently" implemented in most situations.

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 1eb2a495d4624bed0709830af6386c4a25e5ec10..5f256a1e06864d2e022a126592e7848b324ab843 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -240,7 +240,7 @@ EXTEND
      (* Produzioni Aggiunte *)
     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
         GrafiteAst.Assume (loc, id, t)
-    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> t']->
+    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
         GrafiteAst.Suppose (loc, t, id, t1)
     | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
       cont=by_continuation ->