[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, 26 insertions, 0 deletions

diff --git a/vernac/printmod.mli b/vernac/printmod.mli
new file mode 100644
index 0000000000..c7f056063b
--- /dev/null
+++ b/vernac/printmod.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+open Names
+
+(** false iff the module is an element of an open module type *)
+val printable_body : DirPath.t -> bool
+
+val pr_mutual_inductive_body : Environ.env ->
+  MutInd.t -> Declarations.mutual_inductive_body ->
+  UnivNames.univ_name_list option -> Pp.t
+
+type mod_ops =
+  { import_module : export:bool -> ModPath.t -> unit
+  ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit
+  }
+
+val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t
+val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t