Merge branch 'pr/367' into v8.6

Parts of PR#367: Fixing the "beautifier" and checking the
parsing-printing reversibility

2 files changed, 13 insertions, 9 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 6e40e03f5b..fcc30d702f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -219,7 +219,7 @@ module Make
     | ConstrContext ((_,id),c) ->
       hov 0
         (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
-           str "[" ++ prlc c ++ str "]")
+           str "[ " ++ prlc c ++ str " ]")
     | ConstrTypeOf c ->
       hov 1 (keyword "type of" ++ spc() ++ prc c)
     | ConstrTerm c when test c ->
@@ -630,7 +630,8 @@ module Make
         | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
       in
       pr_in
-        (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
+        (prlist_with_sep (fun () -> str",")
+           (fun id -> spc () ++ pr_hyp_location pr_id id) l ++ pr_occs)
 
   let pr_orient b = if b then mt () else str "<- "
 
@@ -675,9 +676,9 @@ module Make
     | Subterm (b,None,a) ->
     (** ppedrot: we don't make difference between [appcontext] and [context]
         anymore, and the interpretation is governed by a flag instead. *)
-      keyword "context" ++ str" [" ++ pr_pat a ++ str "]"
+      keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]"
     | Subterm (b,Some id,a) ->
-      keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+      keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]"
 
   let pr_match_hyps pr_pat = function
     | Hyp (nal,mp) ->
@@ -1216,7 +1217,7 @@ module Make
           | TacNumgoals ->
             keyword "numgoals"
           | (TacCall _|Tacexp _ | TacGeneric _) as a ->
-            str "ltac:(" ++ pr_tac (1,Any) (TacArg (Loc.ghost,a)) ++ str ")"
+            hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a))))
 
         in pr_tac
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3494ad006f..5d6d36d569 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -913,7 +913,7 @@ module Make
       | VernacContext l ->
         return (
           hov 1 (
-            keyword "Context" ++ spc () ++ pr_and_type_binders_arg l)
+            keyword "Context" ++ pr_and_type_binders_arg l)
         )
 
       | VernacDeclareInstances insts ->
@@ -1015,7 +1015,10 @@ module Make
             (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
                prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
                pr_syntax_modifiers
-               (match compat with None -> [] | Some v -> [SetCompatVersion v]))
+               (match compat with
+                | None -> []
+                | Some Flags.Current -> [SetOnlyParsing]
+                | Some v -> [SetCompatVersion v]))
         )
       | VernacDeclareImplicits (q,[]) ->
         return (
@@ -1057,7 +1060,7 @@ module Make
               in
               print_arguments nargs args ++
                 if not (List.is_empty more_implicits) then
-                  str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits
+                  prlist (fun l -> str"," ++ print_implicits l) more_implicits
                 else (mt ()) ++
                 (if not (List.is_empty mods) then str" : " else str"") ++
                   prlist_with_sep (fun () -> str", " ++ spc()) (function
@@ -1128,7 +1131,7 @@ module Make
       | VernacSetAppendOption (na,v) ->
         return (
           hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++
-                   spc() ++ keyword "Append" ++ spc() ++ str v)
+                   spc() ++ keyword "Append" ++ spc() ++ qs v)
         )
       | VernacAddOption (na,l) ->
         return (