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

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 38553b305..f72a7ebc5 100644
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -67,7 +67,10 @@ 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
@@ -145,7 +148,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