X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FlibraryObjects.ml;h=e402f4db214433ce174396929744ba8a4042d2cf;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=7e1dc626f7885afe404fe224310b5c2a60a196e8;hpb=af95d9e68e803244c919fee21877a38ef13c863b;p=helm.git

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index 7e1dc626f..e402f4db2 100644
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -80,7 +80,25 @@ let reset_defaults () =
   true_URIs_ref := default_true_URIs;
   false_URIs_ref := default_false_URIs;
   absurd_URIs_ref := default_absurd_URIs
+;;
+
+let stack = ref [];;
 
+let push () =
+  stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref)::!stack;
+  reset_defaults ()
+;;
+
+let pop () =
+  match !stack with
+  | [] -> raise (Failure "Unable to POP in libraryObjects.ml")
+  | (eq,t,f,a)::tl ->
+      stack := tl;
+      eq_URIs_ref := eq;
+      true_URIs_ref := t;
+      false_URIs_ref := f;
+      absurd_URIs_ref := a
+;;
 
 (**** LOOKUP FUNCTIONS ****)
 let eq_URI () =