# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223070821 14400
# Node ID 6c2607211cee0ce0245b372daabd12e94dbac2ee
# Parent  c49d999fe8066dabf0d1cc91a73a95c38019e375
Expand MoreSpecif

diff -r c49d999fe806 -r 6c2607211cee src/MoreSpecif.v
--- a/src/MoreSpecif.v	Fri Oct 03 15:59:59 2008 -0400
+++ b/src/MoreSpecif.v	Fri Oct 03 17:53:41 2008 -0400
@@ -40,6 +40,9 @@
                            end)
 (right associativity, at level 60) : specif_scope.
 
+Notation "!!" := (inright _ _) : specif_scope.
+Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope.
+
 Notation "x <-- e1 ; e2" := (match e1 with
                                | inright _ => !!
                                | inleft (exist x _) => e2