Release 0.5.9.

[helm.git] / helm / software / components / binaries / matitaprover / matitaprover.ml

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index f72a7ebc5c2520b6217d61f851fba79e96c1e89f..38553b3053aa1c0f43cb8cb648d3e2e458431962 100644 (file)
--- 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