From 93a65415ff582d2ceb5bb9d994edaa6068da8280 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 12:14:59 +0100
Subject: Pre-isolating a notation test to avoid interferences.

---
 interp/notation.ml | 41 ++++++++++++++++++++++++++++++++---------
 1 file changed, 32 insertions(+), 9 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index db8ee5bc18..49403c6e34 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -982,15 +982,38 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
-let uninterp_notations c =
-  List.map_append (fun key -> keymap_find key !notations_key_table)
-    (glob_constr_keys c)
-
-let uninterp_cases_pattern_notations c =
-  keymap_find (cases_pattern_key c) !notations_key_table
-
-let uninterp_ind_pattern_notations ind =
-  keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
+let sort_notations scopes l =
+  let extract_scope l = function
+    | Scope sc -> List.partitioni (fun _i x ->
+                      match x with
+                      | NotationRule (Some sc',_),_,_ -> String.equal sc sc'
+                      | _ -> false) l
+    | SingleNotation ntn -> List.partitioni (fun _i x ->
+                      match x with
+                      | NotationRule (None,ntn'),_,_ -> notation_eq ntn ntn'
+                      | _ -> false) l in
+  let rec aux l scopes =
+    if l == [] then [] (* shortcut *) else
+    match scopes with
+    | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes
+    | [] -> l in
+  aux l scopes
+
+let uninterp_notations scopes c =
+  let scopes = make_current_scopes scopes in
+  let keys = glob_constr_keys c in
+  let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in
+  sort_notations scopes maps
+
+let uninterp_cases_pattern_notations scopes c =
+  let scopes = make_current_scopes scopes in
+  let maps = keymap_find (cases_pattern_key c) !notations_key_table in
+  sort_notations scopes maps
+
+let uninterp_ind_pattern_notations scopes ind =
+  let scopes = make_current_scopes scopes in
+  let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in
+  sort_notations scopes maps
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
-- 
cgit v1.2.3