[states] Move States to vernac

We continue to push state layers upwards, in preparation of a
functional vernacular interpretation.

Now we move `States` and `Printmod` which messes with the global
state as to temporarily create envs with modules.

1 files changed, 0 insertions, 33 deletions

diff --git a/library/states.mli b/library/states.mli
deleted file mode 100644
index fb50a1a8bd..0000000000
--- a/library/states.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** {6 States of the system} *)
-
-(** In that module, we provide functions to get
-  and set the state of the whole system. Internally, it is done by
-  freezing the states of both [Lib] and [Summary]. We provide functions
-  to write and restore state to and from a given file. *)
-
-type state
-val freeze : marshallable:bool -> state
-val unfreeze : state -> unit
-
-val summary_of_state : state -> Summary.frozen
-val lib_of_state : state -> Lib.frozen
-val replace_summary : state -> Summary.frozen -> state
-val replace_lib : state -> Lib.frozen -> state
-
-(** {6 Rollback } *)
-
-(** [with_state_protection f x] applies [f] to [x] and restores the
-  state of the whole system as it was before applying [f] *)
-
-val with_state_protection : ('a -> 'b) -> 'a -> 'b
-