bug fix in subst tactic

[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 3653c46069adc15ff3a2be2aa7edc7ca9693ea1f..7b515472d2ef386385855a7d78abbf6543513618 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -163,9 +163,14 @@ EXTEND
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
-    | IDENT "elim"; what = tactic_term; using = using;
-      (num, idents) = intros_spec ->
-       GrafiteAst.Elim (loc, what, using, num, idents)
+    | IDENT "elim"; what = tactic_term; using = using; 
+       pattern = OPT pattern_spec;
+       (num, idents) = intros_spec ->
+       let pattern = match pattern with
+          | None         -> None, [], Some Ast.UserInput
+          | Some pattern -> pattern   
+       in
+       GrafiteAst.Elim (loc, what, using, pattern, num, idents)
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
        GrafiteAst.ElimType (loc, what, using, num, idents)
@@ -189,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
@@ -330,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";
@@ -344,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:
@@ -358,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: [
@@ -637,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)
     ]
   ];