From eb3f8a09ad53adc744ba7399f5bff875affa5126 Mon Sep 17 00:00:00 2001
From: bertot
Date: Mon, 3 Feb 2003 07:50:47 +0000
Subject: Added a clause for VernacDefineModule, but with an error as result.

This is more work to do to have a complete treatement of the Vernac syntax.


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

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 801f7208e4..e9995e5590 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1666,6 +1666,7 @@ let xlate_vernac =
 
   (* Modules and Module Types *)
   | VernacDeclareModule _ -> xlate_error "TODO: vernac"
+  | VernacDefineModule _ -> xlate_error "TODO: vernac"
   | VernacDeclareModuleType _ -> xlate_error "TODO: vernac"
 
 let rec xlate_vernac_list =
-- 
cgit v1.2.3