Never implemented tactics compare and decide equality purged from the code.

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index e480efd34f1cbfbc77656716ee0f4f9ff0b59f66..73d6bf66ac5e3f8c37865cacbd7719fb092cf8eb 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -140,16 +140,12 @@ EXTEND
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
-    | IDENT "compare"; t = tactic_term ->
-        GrafiteAst.Compare (loc,t)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decide"; IDENT "equality" ->
-        GrafiteAst.DecideEquality loc
     | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
       (num, idents) = intros_spec ->
         let types = match types with None -> [] | Some types -> types in