X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FPreamble.v;h=f83d9a1615a40073c1a6c5eeefbee7a7e841223f;hb=bb960df7c29c851ca9d13f2d0c8f351ac24045ca;hp=17174b3381bb141063119fe039fbf52b5cfee7db;hpb=8c26722a1ee110077968a8a166eb7130266b2035;p=coq-hetmet.git

diff --git a/src/Preamble.v b/src/Preamble.v
index 17174b3..f83d9a1 100644
--- a/src/Preamble.v
+++ b/src/Preamble.v
@@ -109,6 +109,7 @@ Delimit Scope garrow_scope  with garrow.
 Notation "f ○ g"    := (fun x => f(g(x))).
 Notation "?? T"     := (option T).
 Notation "a && b"   := (if a then b else false).
+Notation "a || b"   := (if a then true else b).
 
 (* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *)
 Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100).