User-level support for Gonthier-Ssreflect's "if t then pat then u else v".

1 files changed, 12 insertions, 0 deletions

diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 5e8d2faa5..0c212b025 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -78,6 +78,18 @@ Reserved Notation "{ x : A  |  P  & Q }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  & P  & Q }" (at level 0, x at level 99).
 
+(** Support for Gonthier-Ssreflect's "if c is pat then u else v" *)
+
+Module IfNotations.
+
+Notation "'if' c 'is' p 'then' u 'else' v" :=
+  (match c with p => u | _ => v end)
+  (at level 200, p pattern at level 100).
+
+End IfNotations.
+
+(** Scopes *)
+
 Delimit Scope type_scope with type.
 Delimit Scope function_scope with function.
 Delimit Scope core_scope with core.