The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Victor Porton wrote:
> On the contrary in the above mentioned ZF formalization for Coq can be used 
> together with the rest Coq theories because a set is just a type.
>   

I don't think this is accurate.  CIC and ZF have been proved relatively 
consistent, but this does not yield a practical way to mix the two in 
Coq developments.