5 files changed, 34 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_10904.v b/test-suite/bugs/closed/bug_10904.v
new file mode 100644
index 0000000000..32b25ff726
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10904.v
@@ -0,0 +1,8 @@
+Definition a := fun (P:SProp) (p:P) => p.
+
+Lemma foo : (let k := a in let k' := a in fun (x:nat) y => x) = (let k := a in fun x y => y).
+Proof.
+  Fail reflexivity.
+  match goal with |- ?l = _ => exact_no_check (eq_refl l) end.
+Fail Qed.
+Abort.
diff --git a/test-suite/bugs/closed/bug_6323.v b/test-suite/bugs/closed/bug_6323.v
index fdc33befc6..24feb7155c 100644
--- a/test-suite/bugs/closed/bug_6323.v
+++ b/test-suite/bugs/closed/bug_6323.v
@@ -6,4 +6,5 @@ Goal True.
       simple refine (let id' : { x : X' | True } -> X' := _ in _);
       [ abstract refine (@proj1_sig _ _) | ]
     ].
-Abort.
+  exact I.
+Defined.
diff --git a/test-suite/bugs/closed/bug_9851.v b/test-suite/bugs/closed/bug_9851.v
new file mode 100644
index 0000000000..1f57ce8471
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9851.v
@@ -0,0 +1,18 @@
+Require Import Ring_base.
+Record word : Type := Build_word
+  { rep : Type;
+    zero : rep; one: rep;
+    add : rep -> rep -> rep;
+    sub : rep -> rep -> rep;
+    opp : rep -> rep;
+    mul : rep -> rep -> rep;
+    }.
+Axiom rth
+     : forall (word : word ),
+       @ring_theory (@rep word)
+         (@zero word)
+         (@one word) (@add word)
+         (@mul word) (@sub word)
+         (@opp word) (@eq (@rep word)).
+
+Fail Add Ring wring: (@rth _).
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
new file mode 100644
index 0000000000..473db2d312
--- /dev/null
+++ b/test-suite/output/locate.out
@@ -0,0 +1,3 @@
+Notation
+"b1 && b2" := if b1 then b2 else false (default interpretation)
+"x && y" := andb x y : bool_scope
diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v
new file mode 100644
index 0000000000..af8b0ee193
--- /dev/null
+++ b/test-suite/output/locate.v
@@ -0,0 +1,3 @@
+Set Printing Width 400.
+Notation "b1 && b2" := (if b1 then b2 else false).
+Locate "&&".