The Coq mailing list

["Fabian Pijcke" <fabian.pijcke AT gmail.com>]

Dear list,

I use the tactic "inversion H using myinversionprinciple.".

However, the principle I come with has several flaws. For example, it does not
introduce new variables automatically, and doesn't skip the trivially false
cases.

Is there a way to Check the default induction principle used for an Inductive
type ?

Have a nice day,

Fabian Pijcke