The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I downloaded a theory by Carlos Simpson and tried to compile it with Coq 
83.pl2:
http://arxiv.ccsd.cnrs.fr/e-print/math/0402336v1

$ coq_makefile 
..
$ make
Makefile:170: .depend: No such file or directory
rm -f .depend
coqdep -c -i -I . *.v *.ml *.mli >.depend
coqdep -c -I . -suffix .html *.v >>.depend
coqc  -q  -I .   axioms
coqc  -q  -I .   tactics
coqc  -q  -I .   set_theory
File "./set_theory.v", line 278, characters 19-20:
Error: The reference T was not found in the current environment.
make: *** [set_theory.vo] Error 1

It is strange that it refers to some T defined nowhere.

We need to fix this error.

===

In the original theory of Carlos Simpson (as opposed to rewritten theory by 
José Grimm) every type is a set.

Maybe I'm wrong but it seems to have the convenience that for example 
Set->Set->Prop is a set and there was no need to write explicit type 
conversions.

May we rewrite some of these libraries of theories to bring back that every 
type is a set?

Is my proposal viable?

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