From 5d714a3a78f949fd48c24bec17193bc62d8024a3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Jan 2009 20:14:57 +0000
Subject: Fixing a cosmetic tactic printer bug in passing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11764 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pptactic.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2f102488f5..447bb734a7 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -178,7 +178,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
 	  x)
   | ExtraArgType s -> 
       try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> str " [no printer for " ++ str s ++ str "] "
+      with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
 
 let rec pr_glob_generic prc prlc prtac x =
@@ -223,7 +223,7 @@ let rec pr_glob_generic prc prlc prtac x =
 	  x)
   | ExtraArgType s -> 
       try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> str "[no printer for " ++ str s ++ str "] "
+      with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
 open Closure
 
-- 
cgit v1.2.3