injection_tac and discriminate_tac now replaced by destruct_tac that

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 9373e54b43a1de051f743a2581220677abaf4df8..ab15311dfd219c09bb7af3cc51b920724b62f071 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -160,8 +160,8 @@ EXTEND
        let to_spec id = GrafiteAst.Ident id in
        GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
-    | IDENT "discriminate"; t = tactic_term ->
-        GrafiteAst.Discriminate (loc, t)
+    | 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)
@@ -191,8 +191,6 @@ EXTEND
     | IDENT "goal"; n = int ->
         GrafiteAst.Goal (loc, n)
     | IDENT "id" -> GrafiteAst.IdTac loc
-    | IDENT "injection"; t = tactic_term ->
-        GrafiteAst.Injection (loc, t)
     | IDENT "intro"; ident = OPT IDENT ->
         let idents = match ident with None -> [] | Some id -> [id] in
         GrafiteAst.Intros (loc, Some 1, idents)