Fixing multiple printing bugs with "Notation f x := ..."

- Missing space and bad constr level in "About f"
- Display of arguments missing when used as a pattern notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 5 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 17feae4ed1..87f11030ef 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -458,13 +458,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.glob_constr_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_lglob_constr 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_glob_constr c) ++ fnl ()
 
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "