diff options
author | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:44:20 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:44:20 +0200 |
commit | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (patch) | |
tree | a418d1edb3d53cdb4185b9719b7a70822cf5a24d /parsing/prettyp.ml | |
parent | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (diff) |
Imported Upstream version 8.3.pl2upstream/8.3.pl2
Diffstat (limited to 'parsing/prettyp.ml')
-rw-r--r-- | parsing/prettyp.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index cf83c72a..3fc18219 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: prettyp.ml 13967 2011-04-08 14:08:43Z herbelin $ *) open Pp open Util @@ -460,13 +460,15 @@ let gallina_print_constant_with_infos sp = with_line_skip (print_name_infos (ConstRef sp)) let gallina_print_syntactic_def kn = - let sep = " := " - and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn + let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in let c = Topconstr.rawconstr_of_aconstr dummy_loc a in - str "Notation " ++ pr_qualid qid ++ - prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++ - Constrextern.without_symbols pr_lrawconstr c ++ fnl () + hov 2 + (hov 4 + (str "Notation " ++ pr_qualid qid ++ + prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ + spc () ++ str ":=") ++ + spc () ++ Constrextern.without_symbols pr_rawconstr c) ++ fnl () let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " |