X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN%2Falgebra%2FCoRN%2FSetoids.ma;h=85d134a5ea11a72c0e754fe2d8cbc308b4d3e290;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=43c2d45c433b78a00e302e8ae61c042392f06cab;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma b/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma
index 43c2d45c4..85d134a5e 100644
--- a/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma
+++ b/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma
@@ -47,9 +47,9 @@ record CSetoid : Type \def
    cs_ap    :  relation cs_crr;
    cs_proof :  is_CSetoid cs_crr cs_eq cs_ap}.   
 
-interpretation "setoid equality" 'eq x y = (cs_eq _ x y).
+interpretation "setoid equality" 'eq x y = (cs_eq ? x y).
 
-interpretation "setoid apart" 'neq x y = (cs_ap _ x y).
+interpretation "setoid apart" 'neq x y = (cs_ap ? x y).
 
 (* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness", 
 "cs_neq" e "ap" non sono la stessa cosa? *)