From e260c203fa74a587bd78b2803c8ee046ff3df20a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 12 Jun 2020 04:37:50 +0200
Subject: [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.
---
 library/library.mllib |  2 --
 library/states.ml     | 33 ---------------------------------
 library/states.mli    | 33 ---------------------------------
 3 files changed, 68 deletions(-)
 delete mode 100644 library/states.ml
 delete mode 100644 library/states.mli

(limited to 'library')

diff --git a/library/library.mllib b/library/library.mllib
index a6188f7661..cdc131cfab 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -5,7 +5,5 @@ Summary
 Nametab
 Global
 Lib
-States
-Kindops
 Goptions
 Coqlib
diff --git a/library/states.ml b/library/states.ml
deleted file mode 100644
index b6904263df..0000000000
--- a/library/states.ml
+++ /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)         *)
-(************************************************************************)
-
-type state = Lib.frozen * Summary.frozen
-
-let lib_of_state = fst
-let summary_of_state = snd
-let replace_summary (lib,_) st = lib, st
-let replace_lib (_,st) lib = lib, st
-
-let freeze ~marshallable =
-  (Lib.freeze (), Summary.freeze_summaries ~marshallable)
-
-let unfreeze (fl,fs) =
-  Lib.unfreeze fl;
-  Summary.unfreeze_summaries fs
-
-(* Rollback. *)
-
-let with_state_protection f x =
-  let st = freeze ~marshallable:false in
-  try
-    let a = f x in unfreeze st; a
-  with reraise ->
-    let reraise = Exninfo.capture reraise in
-    (unfreeze st; Exninfo.iraise reraise)
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
-
-- 
cgit v1.2.3