From 4d9375d18d58958d992f76799ad545b800321d78 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 8 Mar 2018 19:11:28 +0100
Subject: Revert "Merge PR #873: New strategy based on open scopes for deciding
 which notation to use among several of them"

This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing
changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
---
 interp/notation.ml | 41 +++++++++--------------------------------
 1 file changed, 9 insertions(+), 32 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index da3ed6b8ca..47d6481350 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -545,38 +545,15 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
-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'),_,_ -> String.equal 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 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 availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
-- 
cgit v1.2.3