From ca04c9042de024eb559e7841dfce1cf67056a145 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 15 Apr 2011 16:46:18 +0000
Subject: Extraction: nicer error when a toplevel module has no body (#2525)

 I thought this situation wasn't possible, hence the Option.get.
 But it's apparently legal to use Declare Module anywhere, even
 outside a Module Type. No idea on how to handle that at extraction
 for the moment, hence a proper "unsupported" error message.

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

(limited to 'plugins/extraction/table.ml')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 4e08079a3b..3dbfa7c02b 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -329,6 +329,12 @@ let error_module_clash mp1 mp2 =
        pr_long_mp mp2 ++ str " have the same ML name.\n" ++
        str "This is not supported yet. Please do some renaming first.")
 
+let error_no_module_expr mp =
+  err (str "The module " ++ pr_long_mp mp
+       ++ str " has no body, it probably comes from\n"
+       ++ str "some Declare Module outside any Module Type.\n"
+       ++ str "This situation is currently unsupported by the extraction.")
+
 let error_unknown_module m =
   err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
 
-- 
cgit v1.2.3