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 fdb37772816c672f1bc400a7664f3ca62aeeb332..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