From fc0e2d6f0430be7dcd74ff737be1722a7c923243 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Jul 2006 08:04:01 +0000
Subject: Suite remplacement VernacDebug par VernacSetOption

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

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2a11f55c9c..024cb59919 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -2035,7 +2035,6 @@ let rec xlate_vernac =
   | VernacExtend (s, l) ->
       CT_user_vernac
        (CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l))
-  | VernacDebug b -> xlate_error "Debug On/Off not supported"
   | VernacList((_, a)::l) -> 
       CT_coerce_COMMAND_LIST_to_COMMAND
 	(CT_command_list(xlate_vernac a, 
-- 
cgit v1.2.3