The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Does the inversion tactic, when it attempts to simplify constraints, 
eliminate constraints that can't possibly apply due to proof 
irrelevance?  I am working in a development where proofs are relevant, 
and am finding that I need to use simple inversion almost all the time 
else important constraint hypotheses that inversion should introduce are 
not appearing.

If inversion is assuming proof irrelevance, is there a way to turn this 
off without forcing one to rely only on simple inversion?

Are there any other tactics that assume proof irrelevance that I should 
avoid, or is there some big setting to make them all stop making that 
assumption?

-- Jonathan