From 3fde88e299a65a87be789ad8cc6ae10d6845a5b4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 3 Oct 2010 13:11:35 +0000
Subject: Fixed a little printing bug with "About" on an undefined constant.

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

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index c4e378826c..d6d2152e56 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -646,16 +646,16 @@ let print_opaque_name qid =
 	print_named_decl (id,c,ty)
 
 let print_about_any k =
-  begin match k with
+  v 0 (match k with
   | Term ref ->
-      print_ref false ref ++ fnl () ++ print_name_infos ref ++
-      print_opacity ref
+      print_ref false ref ++ fnl () ++ print_name_infos ref ++ cut () ++
+      print_opacity ref ++
+      hov 0 (str "Expands to: " ++ pr_located_qualid k)
   | Syntactic kn ->
-      print_syntactic_def kn
+      print_syntactic_def kn ++
+      hov 0 (str "Expands to: " ++ pr_located_qualid k)
   | Dir _ | ModuleType _ | Undefined _ ->
-      mt () end
-  ++
-  hov 0 (str "Expands to: " ++ pr_located_qualid k)
+      hov 0 (pr_located_qualid k))
 
 let print_about = function
   | Genarg.ByNotation (loc,ntn,sc) ->
-- 
cgit v1.2.3