diff options
| author | letouzey | 2007-10-09 20:51:04 +0000 |
|---|---|---|
| committer | letouzey | 2007-10-09 20:51:04 +0000 |
| commit | 962f845da900095720f93b97c3977be96027c82b (patch) | |
| tree | 79cc7d5ca16b6af2fe2818cab4b7171a064b4082 | |
| parent | bfa770fa6077dee42d734232908cd5631feb6af6 (diff) | |
forbid extraction under a module type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10206 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/table.ml | 14 |
1 files 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 |