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=ee5f99610ed7be4c91f32c4835c4ed61ef3e3cbd;hpb=cb3513ef18e52e6e054f8bc99abb833afbb2aee5;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 ee5f99610..85d134a5e 100644
--- a/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma
+++ b/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma
@@ -47,11 +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 = (cic:/matita/algebra/CoRN/Setoids/cs_eq.con _ x y).
+interpretation "setoid equality" 'eq x y = (cs_eq ? x y).
 
-interpretation "setoid apart"
-  'neq x y = (cic:/matita/algebra/CoRN/Setoids/cs_ap.con _ 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? *)