notational update in lambdadelta completed

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / notation / constructors / oplusright_5.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
index 6da02adc1838028ee42305a779f038b13ac5c550..8ea93cad84c35b22ddf97b760e5ebd2aacfc289d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
@@ -16,14 +16,14 @@
 
 notation < "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
   non associative with precedence 47
-  for @{ 'OplusRight $S1 $S2 $hd1 $hd2 $tl }.
+  for @{ 'OPlusRight $S1 $S2 $hd1 $hd2 $tl }.
 
 notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
   non associative with precedence 47
-  for @{ 'OplusRight ? ? $hd1 $hd2 $tl }.
+  for @{ 'OPlusRight ? ? $hd1 $hd2 $tl }.
 (*
 (**) fix pair notation
 notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮{ break term 46 S1, break term 46 S2 } break term 46 tl )"
   non associative with precedence 47
-  for @{ 'OplusRight $S1 $S2 $hd1 $hd2 $tl }.
+  for @{ 'OPlusRight $S1 $S2 $hd1 $hd2 $tl }.
 *)