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/extract_env.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'plugins/extraction/extract_env.ml') 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 -- cgit v1.2.3