X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_engine%2FgrafiteEngine.ml;h=c55bf8d9ebecb5296304548c296d6f42a0b17426;hb=9a17bf0f4213f5f130326d658ce7ee4b41f6d6f2;hp=65dd17b6a096c1e144daf7068e80cf49cba2ce2d;hpb=f4f07dfb8a4e0235bc09698e3df8ff1e9ea7511b;p=helm.git

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 65dd17b6a..c55bf8d9e 100644
--- 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