From feb92894c6be249abadd3303cfca3b258d6f3ea8 Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 29 Sep 2009 15:11:52 +0000
Subject: Add support for Local Declare ML Module

Instead of failing with some obscure error message *after* loading the
module, accept Local Declare ML Module with the usual semantics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12366 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/interface/xlate.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'plugins/interface/xlate.ml')

diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 613c31db71..d294af68d2 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1671,10 +1671,13 @@ let rec xlate_vernac =
       (*ML commands *)
     | VernacAddMLPath (false,str) -> CT_ml_add_path (CT_string str)
     | VernacAddMLPath (true,str) -> CT_rec_ml_add_path (CT_string str)
-    | VernacDeclareMLModule [] -> failwith ""
-    | VernacDeclareMLModule (str :: l) ->
-      CT_ml_declare_modules
-       (CT_string_ne_list (CT_string str, List.map (fun x -> CT_string x) l))
+    | VernacDeclareMLModule (_, []) -> failwith ""
+    | VernacDeclareMLModule (local, (str :: l)) ->
+        let x = CT_string_ne_list (CT_string str, List.map (fun x -> CT_string x) l) in
+        if local then
+          CT_local_ml_declare_modules x
+        else
+          CT_ml_declare_modules x
     | VernacGoal c ->
 	CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (xlate_formula c))
     | VernacAbort (Some (_,id)) ->
-- 
cgit v1.2.3