From 3111aa5721db71d0d4bb2f9717d61723f76bf97e Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 16 Sep 2010 16:00:13 +0000
Subject: Explicit Mod_checking signature

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13422 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/mod_checking.mli | 9 +++++++++
 checker/safe_typing.ml   | 3 +--
 2 files changed, 10 insertions(+), 2 deletions(-)
 create mode 100644 checker/mod_checking.mli

diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
new file mode 100644
index 0000000000..8021ed0f94
--- /dev/null
+++ b/checker/mod_checking.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val check_module : Environ.env -> Names.module_path -> Declarations.module_body -> unit
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 83364aa728..0b3ef54bbd 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Declarations
 open Environ
-open Mod_checking
 
 (************************************************************************)
 (*
@@ -189,7 +188,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;
-  check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
+  Mod_checking.check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
   stamp_library file digest;
   (* We drop proofs once checked *)
 (*  let mb = lighten_module mb in*)
-- 
cgit v1.2.3