X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=0207c9231e058b15d5ab820d21b0bf1719ca2cca;hb=6640fe3db217790d39fd9bf772b0b9fe5170786c;hp=e3ee8d60e0bdb48025c46a84da36e107d7f8e42f;hpb=0e93127aaf63e2312c214a0f8fbbc58a6cd129b7;p=helm.git

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index e3ee8d60e..0207c9231 100644
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -47,10 +47,13 @@ let outside exc_opt =
 exception MetaSubstFailure of string Lazy.t
 exception Uncertain of string Lazy.t
 
-let newmeta,maxmeta = 
+let newmeta,maxmeta,pushmaxmeta,popmaxmeta = 
   let maxmeta = ref 0 in
+  let pushedmetas = ref [] in
   (fun () -> incr maxmeta; !maxmeta),
-  (fun () -> !maxmeta)
+  (fun () -> !maxmeta),
+  (fun () -> pushedmetas := !maxmeta::!pushedmetas; maxmeta := 0),
+  (fun () -> match !pushedmetas with [] -> assert false | hd::tl -> pushedmetas := tl)
 ;;
 
 exception NotFound of [`NotInTheList | `NotWellTyped];;