From 962f845da900095720f93b97c3977be96027c82b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 9 Oct 2007 20:51:04 +0000
Subject: forbid extraction under a module type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10206 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/table.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 1e857a400d..0b2837e322 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -163,13 +163,13 @@ let warning_log_ax r =
 		  spc () ++ str "may lead to incorrect or non-terminating ML terms.")
 
 let check_inside_module () = 
-  try 
-    ignore (Lib.what_is_opened ()); 
-    Options.if_verbose warning
-      ("Extraction inside an opened module is experimental.\n"^
-       "In case of problem, close it first.\n"); 
-    Pp.flush_all ()
-  with Not_found -> ()
+  if Lib.is_modtype () then 
+    err (str "You can't do that within a Module Type." ++ fnl () ++
+	 str "Close it and try again.") 
+  else if Lib.is_module () then 
+    msg_warning
+      (str "Extraction inside an opened module is experimental.\n" ++
+       str "In case of problem, close it first.\n")
 
 let check_inside_section () = 
   if Lib.sections_are_opened () then 
-- 
cgit v1.2.3