From bc25e6178f5bcbd1809ede024f33838a00b56b51 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 18 Mar 2010 19:44:24 +0000
Subject: kills a warning about vo in checker/safe_typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12872 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 8f5d457329..98534e08ca 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -132,7 +132,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
 
 (* When the module is admitted, digests *must* match *)
 let unsafe_import file (dp,mb,depends,engmt as vo) digest =
-(*  if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*)
+  if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*)
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") dp env depends;
   check_engagement env engmt;
-- 
cgit v1.2.3