diff options
| author | herbelin | 2010-10-03 13:11:35 +0000 |
|---|---|---|
| committer | herbelin | 2010-10-03 13:11:35 +0000 |
| commit | 3fde88e299a65a87be789ad8cc6ae10d6845a5b4 (patch) | |
| tree | c36d946d008aa019e7c8806f71fa500cca016eef | |
| parent | 9a7da63b880cbeb3e58af5b2e0b39afcd650c253 (diff) | |
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
| -rw-r--r-- | parsing/prettyp.ml | 14 |
1 files 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) -> |