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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

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