From: Enrico Tassi Date: Wed, 6 May 2009 10:52:37 +0000 (+0000) Subject: updated comment X-Git-Tag: make_still_working~4018 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=91f0c0e84bfe6bf22e960d466e16f7260a2882ee;p=helm.git updated comment --- diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index f7378d13b..3378aa998 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -15,7 +15,8 @@ exception MetaSubstFailure of string Lazy.t exception Uncertain of string Lazy.t (* the delift function takes in input a metavariable index, a local_context - * and a term t, and substitutes every Rel in t with its position in + * and a term t, and substitutes every subterm t' of t with its position + * (searched up-to unification) in * the local_context (which is the Rel moved to the canonical context). * Typically, the list of optional terms is the explicit * substitution that is applied to a metavariable occurrence and the result of