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/ascent.mli |  1 +
 plugins/interface/vtp.ml     |  3 +++
 plugins/interface/xlate.ml   | 11 +++++++----
 3 files changed, 11 insertions(+), 4 deletions(-)

(limited to 'plugins/interface')

diff --git a/plugins/interface/ascent.mli b/plugins/interface/ascent.mli
index f0b68fb7c1..bc615f14ec 100644
--- a/plugins/interface/ascent.mli
+++ b/plugins/interface/ascent.mli
@@ -107,6 +107,7 @@ and ct_COMMAND =
   | CT_mind_decl of ct_CO_IND * ct_IND_SPEC_LIST
   | CT_ml_add_path of ct_STRING
   | CT_ml_declare_modules of ct_STRING_NE_LIST
+  | CT_local_ml_declare_modules of ct_STRING_NE_LIST
   | CT_ml_print_modules
   | CT_ml_print_path
   | CT_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR
diff --git a/plugins/interface/vtp.ml b/plugins/interface/vtp.ml
index 1714440dfb..a84f9ea56a 100644
--- a/plugins/interface/vtp.ml
+++ b/plugins/interface/vtp.ml
@@ -373,6 +373,9 @@ and fCOMMAND = function
 | CT_ml_declare_modules(x1) ->
    fSTRING_NE_LIST x1 ++
    fNODE "ml_declare_modules" 1
+| CT_local_ml_declare_modules(x1) ->
+   fSTRING_NE_LIST x1 ++
+   fNODE "local_ml_declare_modules" 1
 | CT_ml_print_modules -> fNODE "ml_print_modules" 0
 | CT_ml_print_path -> fNODE "ml_print_path" 0
 | CT_module(x1, x2, x3, x4) ->
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