Merge branch 'v8.6'

2 files changed, 18 insertions, 2 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 935e2d076e..a00e4bab30 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -793,6 +793,22 @@ end
 
 let do_not_tag _ x = x
 
+let split_token tag s =
+  let len = String.length s in
+  let rec parse_string off i =
+    if Int.equal i len then
+      if Int.equal off i then mt () else tag (str (String.sub s off (i - off)))
+    else if s.[i] == ' ' then
+      if Int.equal off i then parse_space 1 (succ i)
+      else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i)
+    else parse_string off (succ i)
+  and parse_space spc i =
+    if Int.equal i len then str (String.make spc ' ')
+    else if s.[i] == ' ' then parse_space (succ spc) (succ i)
+    else str (String.make spc ' ') ++ parse_string i (succ i)
+  in
+  parse_string 0 0
+
 (** Instantiating Make with tagging functions that only add style
     information. *)
 include Make (struct
@@ -801,7 +817,7 @@ include Make (struct
     let tag_evar        = tag Tag.evar
     let tag_type        = tag Tag.univ
     let tag_unparsing   = function
-    | UnpTerminal s -> tag Tag.notation
+    | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s
     | _ -> do_not_tag ()
     let tag_constr_expr = do_not_tag
     let tag_path = tag Tag.path
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 0d47b34dfd..40ce28dc0c 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -591,7 +591,7 @@ module Make
           | ShowTree -> keyword "Show Tree"
           | ShowProofNames -> keyword "Show Conjectures"
           | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
-          | ShowMatch id -> keyword "Show Match " ++ pr_lident id
+          | ShowMatch id -> keyword "Show Match " ++ pr_reference id
           | ShowThesis -> keyword "Show Thesis"
         in
         return (pr_showable s)