5 files changed, 61 insertions, 22 deletions

diff --git a/test-suite/bugs/opened/bug_4781.v b/test-suite/bugs/closed/bug_4781.v
index 8b651ac22e..464a3de1b3 100644
--- a/test-suite/bugs/opened/bug_4781.v
+++ b/test-suite/bugs/closed/bug_4781.v
@@ -25,29 +25,29 @@ Goal True.
   let x := match constr:(Set) with ?y => constr:(y) end in
   pose x.
 (* This fails with an error: *)
-  Fail let term := constr:(I) in
+  let term := constr:(I) in
   let T := type of term in
   let x := constr:((_ : abstract_term term) : T) in
   let x := match constr:(x) with ?y => constr:(y) end in
   pose x. (* The command has indeed failed with message:
 Error: Variable y should be bound to a term. *)
 (* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
-  Fail let term := constr:(I) in
+  let term := constr:(I) in
   let T := type of term in
   let x := constr:((_ : abstract_term term) : T) in
   let x := match constr:(x) with ?y => y end in
   pose x.
-  Fail let term := constr:(I) in
+  let term := constr:(I) in
   let T := type of term in
   let x := constr:((_ : abstract_term term) : T) in
   let x := (eval cbv iota in x) in
   pose x.
-  Fail let term := constr:(I) in
+  let term := constr:(I) in
   let T := type of term in
   let x := constr:((_ : abstract_term term) : T) in
   let x := type of x in
   pose x. (* should succeed *)
-  Fail let term := constr:(I) in
+  let term := constr:(I) in
   let T := type of term in
   let x := constr:(_ : abstract_term term) in
   let x := type of x in
@@ -70,7 +70,7 @@ Even stranger, consider:*)
 
 (*This works fine.  But if I change the period to a semicolon, I get:*)
 
-      Fail let term := constr:(I) in
+      let term := constr:(I) in
   let T := type of term in
   let x := constr:((_ : abstract_term term) : T) in
   let y := (eval cbv iota in (let v : T := x in v)) in
@@ -82,7 +82,7 @@ Even stranger, consider:*)
  (* should succeed *)
 (*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)
 
- Fail  let term := constr:(I) in
+  let term := constr:(I) in
   let T := type of term in
   let x := constr:((_ : abstract_term term) : T) in
   let y := (eval cbv iota in (let v : T := x in v)) in
@@ -92,3 +92,5 @@ Even stranger, consider:*)
       let x := (eval cbv delta [x'] in x') in
       let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
       idtac. (* should succeed *)
+  exact I.
+Qed.
diff --git a/test-suite/bugs/closed/bug_7904.v b/test-suite/bugs/closed/bug_7904.v
new file mode 100644
index 0000000000..1e518e2adf
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7904.v
@@ -0,0 +1,13 @@
+
+
+Class abstract_term {T} (x : T) := by_abstract_term : T.
+Hint Extern 0 (@abstract_term ?T ?x) => change T; abstract (exact x) : typeclass_instances.
+
+Goal True.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => y end in
+  pose x as v. (* was Error: Variable x should be bound to a term but is bound to a constr. *)
+  exact v.
+Qed.
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