From 59d27909bc49a1ef65d6b03f2804f13dd47fda4f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:44:43 +0000
Subject: Ajout 'Print Scopes' et 'Bind Scope with classes'

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index afa9226e11..a245a4b635 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1471,6 +1471,7 @@ let xlate_vernac =
 	| PrintTables -> xlate_error "TODO: Print Tables"
         | PrintModuleType _ -> xlate_error "TODO: Print Module Type"
         | PrintModule _ -> xlate_error "TODO: Print Module"
+        | PrintScopes -> xlate_error "TODO: Print Scopes"
         | PrintScope _ -> xlate_error "TODO: Print Scope")
   | VernacBeginSection id ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
@@ -1618,6 +1619,8 @@ let xlate_vernac =
 
    | VernacDelimiters _ -> xlate_error "TODO: Delimiters"
 
+   | VernacBindScope _ -> xlate_error "TODO: Bind Scope"
+
    | VernacNotation _ -> xlate_error "TODO: Notation"
 
    | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
-- 
cgit v1.2.3