diff options
Diffstat (limited to 'interp')
| -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 |