From 6bff5ed8ef6ef6148e035f80e26e60d050e79c43 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 10 Dec 2019 23:10:26 +0100
Subject: Fixing #10750 (anomaly of "Print Visibility" on only-printing
 notations).

---
 interp/notation.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index efb826a76e..5dc1658824 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1872,6 +1872,7 @@ let collect_notations stack =
       | SingleNotation ntn ->
           if List.mem_f notation_eq ntn knownntn then (all,knownntn)
           else
+          try
             let { not_interp  = (_, r); not_location = (_, df) } =
               NotationMap.find ntn (find_scope default_scope).notations in
             let all' = match all with
@@ -1879,7 +1880,8 @@ let collect_notations stack =
                   (s,(df,r)::lonelyntn)::rest
               | _ ->
                   (default_scope,[df,r])::all in
-            (all',ntn::knownntn))
+            (all',ntn::knownntn)
+          with Not_found -> (* e.g. if only printing *) (all,knownntn))
     ([],[]) stack)
 
 let pr_visible_in_scope prglob (scope,ntns) =
-- 
cgit v1.2.3