X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Fmatitaprover%2Fmatitaprover.ml;h=38553b3053aa1c0f43cb8cb648d3e2e458431962;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=f72a7ebc5c2520b6217d61f851fba79e96c1e89f;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index f72a7ebc5..38553b305 100644
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -67,10 +67,7 @@ module MakeBlob(C:LeafComparer) : Terms.Blob
                     (fun x _ m -> embed m x) m args
                 in
                 m, Terms.Node (Terms.Leaf (hash name):: args) 
-        let is_eq = function
-	  | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
-              Some (ty,l,r) 
-	  | _ -> None
+        ;;
         let saturate bo ty = 
           let vars, ty = embed [] ty in
           let _, bo = embed vars bo in
@@ -148,7 +145,7 @@ module Main(P : Paramod.Paramod with type t = leaf) = struct
       ~max_steps:max_int bag ~g_passives:[g_passives] ~passives 
    with
    | P.Error s -> report_error s; 3
-   | P.Unsatisfiable ((bag,_,_,l)::_) -> 
+   | P.Unsatisfiable ((bag,_,l)::_) -> 
          success_msg bag l pp_unit_clause name; 0
    | P.Unsatisfiable ([]) -> 
          report_error "Unsatisfiable but no solution output"; 3