5 files changed, 34 insertions, 5 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.
diff --git a/test-suite/coq-makefile/camldep/run.sh b/test-suite/coq-makefile/camldep/run.sh
index aa62ee56eb..465677a4bf 100755
--- a/test-suite/coq-makefile/camldep/run.sh
+++ b/test-suite/coq-makefile/camldep/run.sh
@@ -13,5 +13,9 @@ mkdir src
 echo '{ let foo = () }' > src/file1.mlg
 echo 'let bar = File1.foo' > src/file2.ml
 coq_makefile -f _CoqProject -o Makefile
-make src/file2.cmx
-[ -f src/file2.cmx ]
+if which ocamlopt >/dev/null 2>&1; then
+    make src/file2.cmx
+    [ -f src/file2.cmx ]
+fi
+make src/file2.cmo
+[ -f src/file2.cmo ]
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/run.sh b/test-suite/coq-makefile/findlib-package-unpacked/run.sh
index e53a7ed0f7..6d7ae15ee2 100755
--- a/test-suite/coq-makefile/findlib-package-unpacked/run.sh
+++ b/test-suite/coq-makefile/findlib-package-unpacked/run.sh
@@ -16,5 +16,7 @@ coq_makefile -f _CoqProject -o Makefile
 cat Makefile.conf
 cat Makefile.local
 make -C findlib/foo
-make
+if which ocamlopt >/dev/null 2>&1; then
+    make
+fi
 make byte