non uniform coercions landed in hints_declaration.ma, setoids and sets library

[helm.git] / helm / software / matita / nlibrary / sets / setoids2.ma

diff --git a/helm/software/matita/nlibrary/sets/setoids2.ma b/helm/software/matita/nlibrary/sets/setoids2.ma
index 578503f6ced96fd59baab50cee6065432b028446..34036a48b37becddc01b1538ab9d4e46e3d831e9 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids2.ma
+++ b/helm/software/matita/nlibrary/sets/setoids2.ma
@@ -40,7 +40,7 @@ notation > "hvbox(a break =_12 b)" non associative with precedence 45
 for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
 *)
 notation > "hvbox(a break =_0 b)" non associative with precedence 45
-for @{ eq_rel ? (eq ?) $a $b }.
+for @{ eq_rel ? (eq0 ?) $a $b }.
 notation > "hvbox(a break =_1 b)" non associative with precedence 45
 for @{ eq_rel1 ? (eq1 ?) $a $b }.
 notation > "hvbox(a break =_2 b)" non associative with precedence 45