X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=7b515472d2ef386385855a7d78abbf6543513618;hb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;hp=3eb64d458fe2892a44f32af5bb1ce5e0af0db1fb;hpb=324d594e5e37081d945d631986447a95a1937634;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 3eb64d458..7b515472d 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -194,8 +194,6 @@ EXTEND
         GrafiteAst.FwdSimpl (loc, hyp, idents)
     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
        GrafiteAst.Generalize (loc,p,id)
-    | IDENT "goal"; n = int ->
-        GrafiteAst.Goal (loc, n)
     | IDENT "id" -> GrafiteAst.IdTac loc
     | IDENT "intro"; ident = OPT IDENT ->
         let idents = match ident with None -> [] | Some id -> [id] in
@@ -335,9 +333,9 @@ EXTEND
           (GrafiteAst.Then (loc, tac, tacs))
       ]
     | "loops" RIGHTA
-      [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
+      [ IDENT "do"; count = int; tac = SELF ->
           GrafiteAst.Do (loc, count, tac)
-      | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
+      | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
       ]
     | "simple" NONA
       [ IDENT "first";
@@ -349,7 +347,7 @@ EXTEND
           GrafiteAst.Solve (loc, tacs)
       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
       | LPAREN; tac = SELF; RPAREN -> tac
-      | tac = tactic -> GrafiteAst.Tactic (loc, tac)
+      | tac = tactic -> tac
       ]
     ];
   punctuation_tactical:
@@ -363,12 +361,11 @@ EXTEND
       | SYMBOL "." -> GrafiteAst.Dot loc
       ]
     ];
-  tactical:
+  non_punctuation_tactical:
     [ "simple" NONA
       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
       | IDENT "skip" -> GrafiteAst.Skip loc
-      | tac = atomic_tactical LEVEL "loops" -> tac
       ]
     ];
   theorem_flavour: [
@@ -642,9 +639,11 @@ EXTEND
   ]];
   executable: [
     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
-    | tac = tactical; punct = punctuation_tactical ->
-        GrafiteAst.Tactical (loc, tac, Some punct)
-    | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
+    | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
+        GrafiteAst.Tactic (loc, Some tac, punct)
+    | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+    | tac = non_punctuation_tactical; punct = punctuation_tactical ->
+        GrafiteAst.NonPunctuationTactical (loc, tac, punct)
     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
     ]
   ];