Merge branch 'pr/367' into v8.6

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

5 files changed, 25 insertions, 17 deletions

diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index c561ecf606..6a8fa8d698 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -50,11 +50,17 @@ let eval_uconstrs ist cs =
   } in
   List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
 
-let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
+let pr_auto_using_raw _ _ _  = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
+let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
+let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob
 
 ARGUMENT EXTEND auto_using
   TYPED AS uconstr_list
   PRINTED BY pr_auto_using
+  RAW_TYPED AS uconstr_list
+  RAW_PRINTED BY pr_auto_using_raw
+  GLOB_TYPED AS uconstr_list
+  GLOB_PRINTED BY pr_auto_using_glob
 | [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ]
 | [ ] -> [ [] ]
 END
@@ -206,8 +212,6 @@ GLOB_PRINTED BY pr_hints_path
 | [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ]
 END
 
-let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
-
 ARGUMENT EXTEND opthints
   TYPED AS preident_list_opt
   PRINTED BY pr_hintbases
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index d570f015eb..aec6a32644 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -419,8 +419,8 @@ let rec comment loc bp = parser bp2
          | [< '')' >] -> push_string "*)"; loc
          | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc
   | [< ''"'; s >] ->
-      let loc = fst (string loc ~comm_level:(Some 0) bp2 0 s)
-      in
+      let loc, len = string loc ~comm_level:(Some 0) bp2 0 s in
+      push_string "\""; push_string (get_buff len); push_string "\"";
       comment loc bp s
   | [< _ = Stream.empty >] ep ->
       let loc = set_loc_pos loc bp ep in
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 95095b09cb..43fac8ad83 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -116,9 +116,9 @@ open Pp
 open Genarg
 open Ppconstr
 open Printer
-let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
-let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
-let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
 
 let warn_deprecated_syntax =
   CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
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 (