Quick patch: the maxmeta is now pushed/popped when compiling an external file.

[helm.git] / matita / components / ng_refiner / nCicMetaSubst.mli

diff --git a/matita/components/ng_refiner/nCicMetaSubst.mli b/matita/components/ng_refiner/nCicMetaSubst.mli
index c9530d42da7305a03dbea015af841c65e97012e9..398325df41fd08e28422b097b068e935d0e3d1e0 100644 (file)
--- a/matita/components/ng_refiner/nCicMetaSubst.mli
+++ b/matita/components/ng_refiner/nCicMetaSubst.mli
@@ -19,6 +19,10 @@ val debug: bool ref
 (* the index of the last created meta *)
 val maxmeta: unit -> int
 
+(* Bad, this should be made functional and put in the status! *)
+val pushmaxmeta: unit -> unit
+val popmaxmeta: unit -> unit
+
 (* the delift function takes in input a metavariable index, a local_context
  * and a term t, and substitutes every subterm t' of t with its position 
  * (searched up-to unification) in
@@ -28,9 +32,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).
  *)