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

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 65dd17b6a096c1e144daf7068e80cf49cba2ce2d..c55bf8d9ebecb5296304548c296d6f42a0b17426 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -67,12 +67,10 @@ let tactic_of_ast ast =
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
   | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
   | GrafiteAst.Contradiction _ -> Tactics.contradiction
-  | GrafiteAst.Compare (_, term) -> Tactics.compare term
   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
   | GrafiteAst.Cut (_, ident, term) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
-  | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
   | GrafiteAst.Decompose (_, types, what, names) -> 
       let to_type = function
          | GrafiteAst.Type (uri, typeno) -> uri, typeno