From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 22 May 2009 12:17:28 +0000 (+0000)
Subject: bugfix in the output notation for eq
X-Git-Tag: make_still_working~3949
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6094ab9349aaa41a8c29c5773a3e756ac819e7f;p=helm.git

bugfix in the output notation for eq
---

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index be61e6650..701903d11 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -80,7 +80,7 @@ for @{ \Pi $_:$a.$b }.
 notation > "hvbox(a break = b)" 
   non associative with precedence 45
 for @{ 'eq ? $a $b }.
-notation < "hvbox(a break maction (=) (=\sub t) b)" 
+notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)" 
   non associative with precedence 45
 for @{ 'eq $t $a $b }.