3 files changed, 25 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_11730.v b/test-suite/bugs/closed/bug_11730.v
new file mode 100644
index 0000000000..f788636f9c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11730.v
@@ -0,0 +1,6 @@
+Set Mangle Names.
+
+Infix "&&&" := andb (at level 40, left associativity).
+(* Error: Variable _0 occurs more than once. *)
+
+Check (_ &&& _).
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
index 25285622a9..bad9d64f65 100644
--- a/test-suite/bugs/closed/bug_9512.v
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -4,9 +4,10 @@ Set Primitive Projections.
 Record params := { width : Z }.
 Definition p : params := Build_params 64.
 
+Definition width' := width.
 Set Printing All.
 
-Goal width p = 0%Z -> width p = 0%Z.
+Lemma foo : width p = 0%Z -> width p = 0%Z.
   intros.
 
   assert_succeeds (enough True; [omega|]).
@@ -16,7 +17,9 @@ Goal width p = 0%Z -> width p = 0%Z.
 (*   ============================ *)
 (*   @eq Z (width p) Z0 *)
 
-  change tt with tt in H.
+  change (width' p = 0%Z) in H;cbv [width'] in H.
+  (* check that we correctly got the compat constant in H *)
+  Fail match goal with H : ?l = _ |- ?l' = _ => constr_eq l l' end.
 
 (*   H : @eq Z (width p) Z0 *)
 (*   ============================ *)
diff --git a/test-suite/bugs/closed/bug_9930.v b/test-suite/bugs/closed/bug_9930.v
new file mode 100644
index 0000000000..042cd69fbe
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9930.v
@@ -0,0 +1,14 @@
+Set Primitive Projections.
+Record params := { width : nat }.
+Definition p : params := Build_params 64.
+
+Lemma foo : width p = 0 -> width p = 0.
+  intros.
+  let e := lazymatch type of H with ?e = 0 => e end in
+  change tt with tt in H;
+  let E := lazymatch type of H with ?E = 0 => E end in
+  idtac "before:" e; idtac "after :" E;
+  (* before: (width p) *)
+  (* after : (width p) *)
+  tryif constr_eq e E then exact H else idtac.
+Qed.