From c6094ab9349aaa41a8c29c5773a3e756ac819e7f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 22 May 2009 12:17:28 +0000 Subject: [PATCH] bugfix in the output notation for eq --- helm/software/matita/core_notation.moo | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 }. -- 2.39.2