diff options
| author | Pierre Roux | 2020-10-20 19:07:22 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:53 +0100 |
| commit | da7787ff4f1b5192b5465ca17ece64f5ebd4f72a (patch) | |
| tree | 14b0a006b87ea609eb2fee81c4e2bd89afc2afb8 /interp/notation.ml | |
| parent | b6214bd4d5d3003e9b60411a717e84277feead24 (diff) | |
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.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 |