From 54c62085a4c08273fb3967d91250df9516d3bfba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 15 Nov 2003 11:49:01 +0000
Subject: Ajout Print Implicit avec depliage du type

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6b4b82e399..5e0bc4d9f9 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1474,7 +1474,8 @@ let xlate_vernac =
         | PrintScopes -> xlate_error "TODO: Print Scopes"
         | PrintScope _ -> xlate_error "TODO: Print Scope"
 	| PrintVisibility _ -> xlate_error "TODO: Print Visibility"
-        | PrintAbout _ -> xlate_error "TODO: Print About")
+        | PrintAbout _ -> xlate_error "TODO: Print About"
+	| _ -> xlate_error "TODO: Print")
   | VernacBeginSection id ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment id -> CT_section_end (xlate_ident id)
-- 
cgit v1.2.3