From da7787ff4f1b5192b5465ca17ece64f5ebd4f72a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 20 Oct 2020 19:07:22 +0200
Subject: Allow multiple primitive notation on the same scope and triggers

Until now, declaring a number or string notation on some trigger
removed all previous notations on the same scope.

Bug discovered by Jason Gross while reviewing #12218.
---
 interp/notation.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 5f6fd62e5c..10e620b58a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1246,7 +1246,6 @@ let cache_prim_token_interpretation (_,infos) =
     String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
   let add_uninterp r =
     let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in
-    let l = List.remove_assoc_f String.equal sc l in
     prim_token_uninterp_infos :=
       GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l)
         !prim_token_uninterp_infos in
-- 
cgit v1.2.3