X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fnotation.ma;h=d4dd5a5de69b5e24dfddf9e47fe6a5ffe6bfe1be;hb=093f9476ddf96034b89e6ad443f74bcc6c067912;hp=d4302a32a8b6d350aff395297974666ec774a62c;hpb=fd991956035d0f1b663aab48325097e53ed9e00e;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma
index d4302a32a..d4dd5a5de 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma
@@ -79,3 +79,7 @@ notation "hvbox( T1 ⇒ break T2 )"
 notation "hvbox( L ⊢ break (term 90 T1) ⇒ break T2 )"
    non associative with precedence 45
    for @{ 'PRed $L $T1 $T2 }.
+
+notation "hvbox( L1 ⊢ ⇒ break L2 )"
+   non associative with precedence 45
+   for @{ 'CPRed $L1 $L2 }.