The Coq mailing list

[Carlos Simpson <Carlos.Simpson AT unice.fr>]

Dear All,

> 
> I wonder if Coq even provides an efficient way of enumerating all 
> axioms, such that it would be reasonable for [omega] to do so.  That 
> technique could still lead to unnecessarily slow proof search, with 
> complex axioms considered in every case, even when they are only needed 
> in a few cases.
> 

This, of course, is the big thing that Coq is missing, namely a
way to access the state of itself in the tactical language. 

---Carlos Simpson