- confluence of parallel substitution (tps) closed! (a bug in an

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / notation.ma

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma
index d4302a32a8b6d350aff395297974666ec774a62c..d4dd5a5de69b5e24dfddf9e47fe6a5ffe6bfe1be 100644 (file)
--- 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 }.