X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=64a96f82aefdcdb4f11a665c3316538b37519f07;hb=d35d134356645a09eb72db6e484f3df583123af1;hp=f15a0cee61a16c3cfb5630ae0c4163bdb95ab01e;hpb=22d39afadb3027477e4a42c315ec10518cbf47ed;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index f15a0cee6..64a96f82a 100644
--- 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