From: Alberto Griggio <griggio@fbk.eu>
Date: Tue, 13 Dec 2005 11:09:45 +0000 (+0000)
Subject: added comment explaining the meaning of the return value of find_matches
X-Git-Tag: make_still_working~8009
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a32b0ea407ce62999f8cfa335cb6f4a8f905a38a;p=helm.git

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 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