3 files changed, 39 insertions, 15 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index d58e4bf2d6..94016e170b 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -45,3 +45,5 @@ fun x : nat => (x.-1)%pred
      : Prop
 ##
      : Prop
+Notation Cn := Foo.FooCn
+Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 61206b6dd0..309115848f 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -164,3 +164,20 @@ Open Scope my_scope.
 Check ##.
 
 End H.
+
+(* Fixing a bug reported by G. Gonthier in #9207 *)
+
+Module J.
+
+Module Import Mfoo.
+Module Foo.
+Definition FooCn := 2.
+Module Bar.
+Notation Cn := FooCn.
+End Bar.
+End Foo.
+Export Foo.Bar.
+End Mfoo.
+About Cn.
+
+End J.
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
index 7f9e6cc6e0..d0b8d21b69 100644
--- a/test-suite/unit-tests/printing/proof_diffs_test.ml
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -51,23 +51,28 @@ let t () =
   assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed
 let _ = add_test "diff_str add/remove" t
 
-(* example of a limitation, not really a test *)
-let t () =
-  try
-    let _ = diff_str "a" ">" in
-    assert_failure "unlexable string gives an exception"
-  with _ -> ()
-let _ = add_test "diff_str unlexable" t
-
-(* problematic examples for tokenize_string:
-   comments omitted
-   quoted string loses quote marks (are escapes supported/handled?)
-   char constant split into 2
+(* lexer tweaks:
+   comments are lexed as multiple tokens
+   strings tokens include begin/end quotes and embedded ""
+   single multibyte characters returned even if they're not keywords
+
+   inputs that give a lexer failure (but no use case needs them yet):
+     ".12"
+     unterminated string
+     invalid UTF-8 sequences
    *)
 let t () =
-  List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx");
-  cprintf "\n"
-let _ = add_test "tokenize_string examples" t
+  let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж > ∃ 'c' xx" in
+  let toks = tokenize_string str in
+  (*List.iter (fun x -> cprintf "'%s' " x) toks;*)
+  (*cprintf "\n";*)
+  let str_no_white = String.concat "" (String.split_on_char ' ' str) in
+  assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks);
+  List.iter (fun s ->
+    assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks))
+    [ "(*"; "()"; ":="]
+
+let _ = add_test "tokenize_string/diff_mode in lexer" t
 
 open Pp