X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=90abc0a89e435f26283041daf4737db03b9150f3;hb=185541ccf10a6c4bf69b3db36fdc4ebc09e4cc42;hp=c1b347071b799ce5ed9630f32ffc15672cd72b15;hpb=b6ceb877c05d27705ef163488aee38e60a86886c;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index c1b347071..90abc0a89 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -239,7 +239,9 @@ EXTEND
     | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
     | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
     | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
-    | IDENT "assume"; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
+    | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.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'] -> G.NTactic (loc,[G.Suppose (loc,t,id,t1)])
     ]
   ];
   auto_fixed_param: [