From 06d096b3ff3dff8cca216091c0c5ffa3a7530e1d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 9 Jul 2012 18:17:40 +0000
Subject: Avoid a warning about unprintable new command Print Namespace

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

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d7b36d2878..2d0173d198 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -909,6 +909,7 @@ let rec pr_vernac = function
          term *)
 	| PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
 	    ++ spc() ++ pr_smart_global qid
+	| PrintNamespace dp -> str"Print Namespace" ++ pr_dirpath dp
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc ->
-- 
cgit v1.2.3