nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / CoRN / algebra / CoRN / Setoids.ma

diff --git a/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma b/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma
index ee5f99610ed7be4c91f32c4835c4ed61ef3e3cbd..85d134a5ea11a72c0e754fe2d8cbc308b4d3e290 100644 (file)
--- 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? *)