X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCOrdCauchy.ma;h=70c46d57a83f1813c53cebbbbada36d76d82a8a6;hb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;hp=5f5e5091c707b57a3752472e73af46d0c3e2a386;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma index 5f5e5091c..70c46d57a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma @@ -70,7 +70,7 @@ with the coercions inline "cic:/CoRN/algebra/COrdCauchy/CauchySeq.ind". -coercion "cic:/matita/CoRN-Decl/algebra/COrdCauchy/CS_seq.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/COrdCauchy/CS_seq.con 0 (* compounds *). inline "cic:/CoRN/algebra/COrdCauchy/SeqLimit.con".