1 files changed, 10 insertions, 0 deletions
diff --git a/tests/src/matches.rs b/tests/src/matches.rs
new file mode 100644
index 00000000..5710a604
--- /dev/null
+++ b/tests/src/matches.rs
@@ -0,0 +1,10 @@
+//@ [coq] skip
+//@ [coq,fstar] subdir=misc
+//^ note: coq gives "invalid notation for pattern"
+fn match_u32(x: u32) -> u32 {
+    match x {
+        0 => 0,
+        1 => 1,
+        _ => 2,
+    }
+}