The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I have the following trouble (not exactly this, but similar):

I have sources (.v) files where the notation (plus A B) abounds.

I want to convert it into a visible format (for example, HTML or PDF) with 
all (plus A B) replaced with A+B.

Can this be done easily?

Now about the real problem:

We have a ZF(C) formalization:
See a .tar file with the theory at:
http://arxiv.ccsd.cnrs.fr/e-print/math/0402336v1
from the article:
http://arxiv.ccsd.cnrs.fr/abs/math/0402336v1

It is a ZF formalization which I wish to use, but it has no infix notation 
for operations.

Also that formalization has the following deficiency:

The type of sets is called "E". It should be rewritten to something longer, 
like "ZF_set".

I think about rewriting that ZF package myself, or maybe to abandon my 
attempt to be involved in Coq theories development, because I don't like 
setoid approach.

Well, maybe somebody can say me something positive about setoids? Maybe I 
hate setoids in vain.

-- 
Victor Porton - http://portonvictor.org