The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/23/2014 02:15 PM, Fabian Pijcke wrote:
> 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 ?

You mean, just to examine an existing one to see how it is defined? 
Try:  Print nat_ind.

-- Jonathan