From a7b406bccfd51d7afee1f26ecfe38002be3b76f2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 7 Feb 2019 08:06:20 +0100
Subject: Fix Locate printing regression

Fixes #9428. (Again.)

This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them.
Corrects a 8.9.1 → 8.10.0 regression.

(cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)
---
 interp/notation.ml           | 2 +-
 test-suite/output/locate.out | 3 +++
 test-suite/output/locate.v   | 3 +++
 3 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/output/locate.out
 create mode 100644 test-suite/output/locate.v

diff --git a/interp/notation.ml b/interp/notation.ml
index ea2173860d..70d3e4175e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1836,7 +1836,7 @@ let locate_notation prglob ntn scope =
     str "Notation" ++ fnl () ++
     prlist_with_sep fnl (fun (ntn,l) ->
       let scope = find_default ntn scopes in
-      prlist
+      prlist_with_sep fnl
 	(fun (sc,r,(_,df)) ->
 	  hov 0 (
 	    pr_notation_info prglob df r ++
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
new file mode 100644
index 0000000000..473db2d312
--- /dev/null
+++ b/test-suite/output/locate.out
@@ -0,0 +1,3 @@
+Notation
+"b1 && b2" := if b1 then b2 else false (default interpretation)
+"x && y" := andb x y : bool_scope
diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v
new file mode 100644
index 0000000000..af8b0ee193
--- /dev/null
+++ b/test-suite/output/locate.v
@@ -0,0 +1,3 @@
+Set Printing Width 400.
+Notation "b1 && b2" := (if b1 then b2 else false).
+Locate "&&".
-- 
cgit v1.2.3