diff options
| -rw-r--r-- | interp/notation.ml | 1 | ||||
| -rw-r--r-- | test-suite/output/StringSyntax.out | 6 | ||||
| -rw-r--r-- | test-suite/output/StringSyntax.v | 20 |
3 files changed, 26 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 diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index 125c1bc927..68ee7cfeb5 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -1096,3 +1096,9 @@ Expects a single character or a three-digit ASCII code. : nat The command has indeed failed with message: Expects a single character or a three-digit ASCII code. +"abc" + : string2 +"abc" : string2 + : string2 +"abc" : string1 + : string1 diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v index 49584487a3..a1ffe69527 100644 --- a/test-suite/output/StringSyntax.v +++ b/test-suite/output/StringSyntax.v @@ -95,3 +95,23 @@ Check "255". Fail Check "256". End Test3. + +(* Test overlapping string notations *) +Module Test4. + +Notation string1 := (list Byte.byte). +Definition id_string1 := @id string1. + +String Notation string1 id_string1 id_string1 : list_scope. + +Notation string2 := (list Ascii.ascii). +Definition a2b := List.map byte_of_ascii. +Definition b2a := List.map ascii_of_byte. + +String Notation string2 b2a a2b : list_scope. + +Check "abc"%list. +Check ["a";"b";"c"]%char%list : string2. +Check ["a";"b";"c"]%byte%list : string1. + +End Test4. |