The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Did you try to "Set Printing All" to check all the hidden variables
that might not have been instanciated ?
Do you know with which version of Coq this code is known to compile ?

Best,
Vincent

2011/11/6 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
>