1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3092.v b/test-suite/bugs/opened/3092.v
new file mode 100644
index 00000000..9db21d15
--- /dev/null
+++ b/test-suite/bugs/opened/3092.v
@@ -0,0 +1,9 @@
+Fail Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
+  match H1 with
+  | le_n      => le_n (pred _)
+  | le_S _ H2 =>
+    match n2 with
+    | 0   => fun H3 => H3
+    | S _ => le_S _ _
+    end (le_pred _ _ H2)
+  end.