From 17c3f8e2d339e5b6f60c89ad17e578d786d2b9ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 15:14:23 +0100
Subject: More on fixing #5098 (preserving printing of "in hyp").

---
 printing/pptactic.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 6e40e03f5b..4b86381b49 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -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 "<- "
 
-- 
cgit v1.2.3


From 4e551415f20ad696c319b32b349e4499c2505388 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 17:58:07 +0100
Subject: Protect printing of ltac's "context [...]" from possible collision
 with user-level notations by inserting spaces.

---
 printing/pptactic.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 4b86381b49..fedc62f44f 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 ->
@@ -676,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) ->
-- 
cgit v1.2.3


From 1c5e311d6a92deb66ba412c56516a4b71a513e01 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 15:35:05 +0100
Subject: Fixing printing of "only parsing" in abbreviations.

---
 printing/ppvernac.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3494ad006f..be15879184 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -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 (
-- 
cgit v1.2.3


From 00f1839a2cee1cb1fa4dc207391c4a5bb588f71a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 15:40:40 +0100
Subject: Fixing space in printing several list of implicit arguments.

---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index be15879184..75271e21ea 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1060,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
-- 
cgit v1.2.3


From a4db30e1cd6c21a466549835a86d61f95db36c82 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Apr 2016 22:24:59 +0200
Subject: Fixing printers for pr_auto_using and pr_firstorder_using.

---
 ltac/g_auto.ml4                 | 10 +++++++---
 plugins/firstorder/g_ground.ml4 |  6 +++---
 2 files changed, 10 insertions(+), 6 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/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"
-- 
cgit v1.2.3


From edb7a97487cb5e38bb284472eacfd1b58fa97f84 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Nov 2016 07:00:31 +0100
Subject: Fixing space in printing "Context".

---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 75271e21ea..9533833212 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 ->
-- 
cgit v1.2.3


From ab3b0de5902082f7e692901979aa8330394c2f26 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Nov 2016 12:58:02 +0100
Subject: Fixing printing of "Set Warnings Append".

---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 9533833212..5d6d36d569 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1131,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 (
-- 
cgit v1.2.3


From afab44873b7861d542cc0146d2bb8099d513f008 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 15:34:39 +0100
Subject: Fixing printing of "ltac:" in tactics after surrounding parentheses
 became mandatory.

---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index fedc62f44f..fcc30d702f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1217,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
 
-- 
cgit v1.2.3


From 7e8434765ca1289aeb3a5200e791c9ced0acfde4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 15:54:55 +0100
Subject: Fixing lexing of strings in comments for beautifier.

Was a bug introduced in 0ad6edc1.
---
 parsing/cLexer.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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
-- 
cgit v1.2.3