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 43c2d45c433b78a00e302e8ae61c042392f06cab..85d134a5ea11a72c0e754fe2d8cbc308b4d3e290 100644 (file)
--- 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? *)