2 files changed, 25 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_10917.v b/test-suite/bugs/closed/bug_10917.v
new file mode 100644
index 0000000000..cdb132ede0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10917.v
@@ -0,0 +1,4 @@
+(* This was raising an anomaly *)
+
+Definition m (h : 0 = 1) P : P 1 -> P 0 :=
+  fun H => match h, H with end.
diff --git a/test-suite/bugs/closed/bug_9741.v b/test-suite/bugs/closed/bug_9741.v
new file mode 100644
index 0000000000..247155d8b3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9741.v
@@ -0,0 +1,21 @@
+(* This was failing at parsing *)
+
+Notation "'a'" := tt (only printing).
+Goal True. let a := constr:(1+1) in idtac a. Abort.
+
+(* Idem *)
+
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.ZArith.
+Open Scope string_scope.
+
+Axiom Ox: string -> Z.
+
+Axiom isMMIOAddr: Z -> Prop.
+
+Notation "'Ox' a" := (Ox a) (only printing, at level 10, format "'Ox' a").
+
+Goal False.
+  set (f := isMMIOAddr).
+  set (x := f (Ox "0018")).
+Abort.