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