From 75b352c0783d5a0c3d2ff15ee46de005cd1e17e5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 11 Jan 2007 19:15:24 +0000
Subject: Petit oubli dans commit 9474

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

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e823a40d15..807a3168c0 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -754,7 +754,8 @@ let rec pr_vernac = function
       let r = Nametab.global q in
       Impargs.declare_manual_implicits local r l;
       let imps = Impargs.implicits_of_global r in
-      hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++
+      hov 1 (str"Implicit Arguments" ++ pr_non_globality local ++
+      spc() ++ pr_reference q ++ spc() ++
              str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]")
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Type" ++
-- 
cgit v1.2.3