]> matita.cs.unibo.it Git - helm.git/commitdiff
Comment is now up-to-date.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 1 Jun 2011 12:57:28 +0000 (12:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 1 Jun 2011 12:57:28 +0000 (12:57 +0000)
matita/components/ng_refiner/nCicMetaSubst.mli

index c9530d42da7305a03dbea015af841c65e97012e9..fdb37772816c672f1bc400a7664f3ca62aeeb332 100644 (file)
@@ -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).
  *)