From 91f0c0e84bfe6bf22e960d466e16f7260a2882ee Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 May 2009 10:52:37 +0000 Subject: [PATCH] updated comment --- helm/software/components/ng_refiner/nCicMetaSubst.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2