From: Ferruccio Guidi Date: Tue, 5 Oct 2021 22:53:00 +0000 (+0200) Subject: update in ground X-Git-Tag: make_still_working~135 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cab35e3d6c09d266c1372b5cc9a0045578bae79b;p=helm.git update in ground + minor bug fixed in a notation --- diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma index ede24a0fe..5ccb16c4b 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma @@ -14,7 +14,7 @@ (* GROUND NOTATION **********************************************************) -notation < "hvbox( f1 ≐ break term 46 f2 )" +notation < "hvbox( term 46 f1 ≐ break term 46 f2 )" non associative with precedence 45 for @{ 'DotEq $A $B $f1 $f2 }.