From a32b0ea407ce62999f8cfa335cb6f4a8f905a38a Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Tue, 13 Dec 2005 11:09:45 +0000 Subject: [PATCH] added comment explaining the meaning of the return value of find_matches --- helm/ocaml/paramodulation/indexing.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) 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 -- 2.39.2