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