The Coq mailing list

[Jason Hickey <jyh AT cs.caltech.edu>]

> Jean-Christophe Filliatre wrote:
>
> > In  the Coq  architecture, the  correctness is  ensured at  the kernel
> > level,  once  the  proof  is  completed.   To  be  more  precise,  the
> > validation above will build the proof  term once the proof is done and
> > this proof term will be type-checked by the kernel.

My apologies, I had been thinking in terms of type theories where 
membership is undecidable...

In Coq, it really doesn't matter how tactics or validations work.  All 
that matters is, by hook or by crook, one finds a proof term.  In the 
end, the only thing that matters is that the type checker is correct. 
Many thanks for answering me Jean-Christophe!

Jason

--
Jason Hickey                  http://www.cs.caltech.edu/~jyh
Caltech Computer Science      Tel: 626-395-6568 FAX: 626-792-4257