Checker: vo validation is now done in check.ml (and always)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16402 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 6 deletions

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 7c96fda5b..b3060c153 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -60,8 +60,6 @@ let check_imports f caller env needed =
   in
   Array.iter check needed
 
-open Validate
-
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
    that could change the .vo file between the time it was read and
@@ -71,10 +69,7 @@ let stamp_library file digest = ()
 
 (* When the module is checked, digests do not need to match, but a
    warning is issued in case of mismatch *)
-let import file clib table digest =
-  Validate.validate !Flags.debug Values.v_compiled_lib clib;
-  Validate.validate !Flags.debug (Values.Array Values.v_constr) table;
-  Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush ();
+let import file clib digest =
   let env = !genv in
   check_imports msg_warning clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;