X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fnotation%2Fconstructors%2Foplusright_5.ma;h=8ea93cad84c35b22ddf97b760e5ebd2aacfc289d;hp=6da02adc1838028ee42305a779f038b13ac5c550;hb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;hpb=b598b37379baabef24ae511596be7f740cbb0c2e

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 6da02adc1..8ea93cad8 100644
--- 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 }.
 *)