added comment explaining the meaning of the return value of find_matches

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 1d2d6a9048a12361851620fdf7bd461e47755ac9..a1b9edac852ba37f775abddbdd159103bc852e0c 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -153,6 +153,22 @@ let match_unif_time_no = ref 0.;;
   termty can be Implicit if it is not needed. The result (one of the sides of
   the equality, actually) should be not greater (wrt the term ordering) than
   term
+
+  Format of the return value:
+
+  (term to substitute, [Cic.Rel 1 properly lifted - see the various
+                        build_newtarget functions inside the various
+                        demodulation_* functions]
+   substitution used for the matching,
+   metasenv,
+   ugraph, [substitution, metasenv and ugraph have the same meaning as those
+   returned by CicUnification.fo_unif]
+   (equality where the matching term was found, [i.e. the equality to use as
+                                                rewrite rule]
+    uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
+         the equality: this is used to build the proof term, again see one of
+         the build_newtarget functions]
+   ))
 *)
 let rec find_matches metasenv context ugraph lift_amount term termty =
   let module C = Cic in