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 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/interface/ascent.mli')

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