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/vtp.ml | 3 +++
 1 file changed, 3 insertions(+)

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

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) ->
-- 
cgit v1.2.3