Tracing mechanism for auto. Interface changed to solve an ambiguity between

[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 38553b3053aa1c0f43cb8cb648d3e2e458431962..f72a7ebc5c2520b6217d61f851fba79e96c1e89f 100644 (file)
--- 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