From 4b02fbd92ec47f1477db71425d2627898019cd5d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 Oct 2018 19:46:41 +0200
Subject: Fixing missing newline in display of Locate for notations.

---
 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 ea6d0f8871..2a095d7466 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1702,7 +1702,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