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 () =