+let history = ref [];;
+
+let push () =
+ history := (!parser_ref_counter,!rule_ids_to_items) :: !history;
+ parser_ref_counter := initial_parser_ref_counter ();
+ rule_ids_to_items := initial_rule_ids_to_items ();
+ TermContentPres.push ();
+ TermAcicContent.push ();
+ CicNotationParser.push ()
+;;
+
+let pop () =
+ TermContentPres.pop ();
+ TermAcicContent.pop ();
+ CicNotationParser.pop ();
+ match !history with
+ | [] -> assert false
+ | (prc,riti) :: tail ->
+ parser_ref_counter := prc;
+ rule_ids_to_items := riti;
+ history := tail;
+;;