updated dependences

[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 1a11ec62f0d788e06a15c55d3c3f3453ccb73e7d..1c85b567d48feb17d98064632c60718f4531f15d 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -231,6 +231,17 @@ EXTEND
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->
         GrafiteAst.Transitivity (loc, t)
+     (* Produzioni Aggiunte *)
+    | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
+        GrafiteAst.Assume (loc, id, t)
+    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+        GrafiteAst.Suppose (loc, t, id)
+    | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+        GrafiteAst.By_term_we_proved (loc, t, ty, id)
+    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+        GrafiteAst.We_need_to_prove (loc, t, id)
+    | IDENT "by" ; t = tactic_term ; IDENT "done" ->
+        GrafiteAst.Bydone (loc, t)
     ]
   ];
   atomic_tactical: