X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.mli;h=fdb37772816c672f1bc400a7664f3ca62aeeb332;hb=41dfa9c8a69428f59683f5ab964b217c67ebe46e;hp=c9530d42da7305a03dbea015af841c65e97012e9;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

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).
  *)