added comment explaining the meaning of the return value of get_candidates

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index a1b9edac852ba37f775abddbdd159103bc852e0c..cb20afd812b9ab54567ca32e3ae0d574d259f955 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -125,6 +125,19 @@ let index = Discrimination_tree.index
 and remove_index = Discrimination_tree.remove_index
 and in_index = Discrimination_tree.in_index;;
 
+(* returns a list of all the equalities in the tree that are in relation
+   "mode" with the given term, where mode can be either Matching or
+   Unification.
+
+   Format of the return value: list of tuples in the form:
+   (position - Left or Right - of the term that matched the given one in this
+     equality,
+    equality found)
+   
+   Note that if equality is "left = right", if the ordering is left > right,
+   the position will always be Left, and if the ordering is left < right,
+   position will be Right.
+*)
 let get_candidates mode tree term =
   let t1 = Unix.gettimeofday () in
   let res =
@@ -135,7 +148,7 @@ let get_candidates mode tree term =
     in
     Discrimination_tree.PosEqSet.elements s
   in
-(*   print_candidates mode term res; *)
+  (*   print_candidates mode term res; *)
 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 (*   print_newline (); *)
   let t2 = Unix.gettimeofday () in