From 9f3fc5d04b69f0c6bf6eec56c32ed11a218dde61 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 17 Jul 2013 15:31:25 +0000
Subject: Extraction : message about lack of support for toplevel Include

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

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index add5428b5c..fae5c7e670 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -43,6 +43,7 @@ let toplevel_env () =
 	  | "MODULE TYPE" ->
             let modtype = Global.lookup_modtype (MPdot (mp, l)) in
             Some (l, SFBmodtype modtype)
+          | "INCLUDE" -> error "No extraction of toplevel Include yet."
 	  | _ -> None
         end
     | _ -> None
-- 
cgit v1.2.3