Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5532.v b/test-suite/bugs/closed/5532.v
new file mode 100644
index 0000000000..ee5446e548
--- /dev/null
+++ b/test-suite/bugs/closed/5532.v
@@ -0,0 +1,15 @@
+(* A wish granted by the new support for patterns in notations *)
+
+Local Notation mkmatch0 e p
+  := match e with
+     | p => true
+     | _ => false
+     end.
+Local Notation "'mkmatch' [[ e ]] [[ p ]]"
+  := match e with
+     | p => true
+     | _ => false
+     end
+       (at level 0, p pattern).
+Check mkmatch0 _ ((0, 0)%core).
+Check mkmatch [[ _ ]] [[ ((0, 0)%core) ]].