The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Marko Malikoviæ wrote:
> Can someone explain to me whether is the standard that omega does not take
> the axioms into account?
>    

This behavior doesn't surprise me.  I've assumed that [omega] only works 
with information appearing in the proof goal, and that's certainly what 
you're seeing here.  You can easily convert an axiom into a hypothesis 
by running [generalize] on it.

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.