From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 1 Jul 2010 17:21:14 +0200
Subject: Imported Upstream version 8.2pl2+dfsg

---
 parsing/pptactic.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing/pptactic.ml')

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3b433498..f52ebc76 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: pptactic.ml 12581 2009-12-13 15:02:33Z herbelin $ *)
 
 open Pp
 open Names
@@ -378,7 +378,7 @@ let pr_as_ipat = function
 
 let pr_as_name = function
   | Anonymous -> mt ()
-  | Name id -> str "as " ++ pr_lident (dummy_loc,id)
+  | Name id -> str " as " ++ pr_lident (dummy_loc,id)
 
 let pr_pose_as_style prc na c =
   spc() ++ prc c ++ pr_as_name na
-- 
cgit v1.2.3