modifications/fixes for the integration with auto

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index f15a0cee61a16c3cfb5630ae0c4163bdb95ab01e..64a96f82aefdcdb4f11a665c3316538b37519f07 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -116,6 +116,8 @@ let get_candidates mode tree term =
     Discrimination_tree.PosEqSet.elements s
   in
 (*   print_candidates mode term res; *)
+(*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
+(*   print_newline (); *)
   let t2 = Unix.gettimeofday () in
   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
   res
@@ -148,7 +150,7 @@ let rec find_matches metasenv context ugraph lift_amount term =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
             try
-              let r = 
+              let r =
                 Inference.matching (metasenv @ metas) context
                   term (S.lift lift_amount c) ugraph in
               let t2 = Unix.gettimeofday () in