From b41c4f4faec7b4b45bbaed3c0fcfb7ed9570ae59 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 1 Jun 2011 12:57:28 +0000 Subject: [PATCH] Comment is now up-to-date. --- matita/components/ng_refiner/nCicMetaSubst.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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). *) -- 2.39.2