X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;fp=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=a1b9edac852ba37f775abddbdd159103bc852e0c;hb=a32b0ea407ce62999f8cfa335cb6f4a8f905a38a;hp=1d2d6a9048a12361851620fdf7bd461e47755ac9;hpb=2765b4ab727995efeebb972973d6032b06095845;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 1d2d6a904..a1b9edac8 100644
--- 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