X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.mli;h=398325df41fd08e28422b097b068e935d0e3d1e0;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=fdb37772816c672f1bc400a7664f3ca62aeeb332;hpb=b41c4f4faec7b4b45bbaed3c0fcfb7ed9570ae59;p=helm.git

diff --git a/matita/components/ng_refiner/nCicMetaSubst.mli b/matita/components/ng_refiner/nCicMetaSubst.mli
index fdb377728..398325df4 100644
--- 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