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

1 files changed, 11 insertions, 4 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 1263055665..bc9047c0ab 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -339,10 +339,17 @@ and extract_seb env mp all = function
   | SEBwith (_,_) -> anomaly "Not available yet"
 
 and extract_module env mp all mb =
-  (* [mb.mod_expr <> None ], since we look at modules from outside. *)
-  (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
-  { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr);
-    ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
+  (* A module has an empty [mod_expr] when :
+     - it is a module variable (for instance X inside a Module F [X:SIG])
+     - it is a module assumption (Declare Module).
+     Since we look at modules from outside, we shouldn't have variables.
+     But a Declare Module at toplevel seems legal (cf #2525). For the
+     moment we don't support this situation. *)
+  match mb.mod_expr with
+    | None -> error_no_module_expr mp
+    | Some me ->
+      { ml_mod_expr = extract_seb env mp all me;
+	ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
 
 
 let unpack = function MEstruct (_,sel) -> sel | _ -> assert false