From: Claudio Sacerdoti Coen Date: Wed, 1 Jun 2011 12:57:28 +0000 (+0000) Subject: Comment is now up-to-date. X-Git-Tag: make_still_working~2471 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b41c4f4faec7b4b45bbaed3c0fcfb7ed9570ae59;p=helm.git Comment is now up-to-date. --- diff --git a/matita/components/ng_refiner/nCicMetaSubst.mli b/matita/components/ng_refiner/nCicMetaSubst.mli index c9530d42d..fdb377728 100644 --- a/matita/components/ng_refiner/nCicMetaSubst.mli +++ b/matita/components/ng_refiner/nCicMetaSubst.mli @@ -28,9 +28,11 @@ val maxmeta: unit -> int * the delift function is a term the implicit variable can be substituted with * to make the term [t] unifiable with the metavariable occurrence. In general, * the problem is undecidable if we consider equivalence in place of alpha - * convertibility. Our implementation, though, is even weaker than alpha + * convertibility. + * The old implementation, though, is even weaker than alpha * convertibility, since it replace the term [tk] if and only if [tk] is a Rel * (missing all the other cases). Does this matter in practice? + * The new experimental implementation, instead, works up to unification. * The metavariable index is the index of the metavariable that must not occur * in the term (for occur check). *)