From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 27 Feb 2013 20:19:04 +0000 (+0000)
Subject: Quick patch: the maxmeta is now pushed/popped when compiling an external file.
X-Git-Tag: make_still_working~1240
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=6640fe3db217790d39fd9bf772b0b9fe5170786c

Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.
---

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];;
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