The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/26/2015 04:28 PM, Jason Gross wrote:
> On Thu, Mar 26, 2015 at 4:18 PM, Jonathan Leivent 
> <jonikelee AT gmail.com>
> wrote:
>
> > On second thought, it isn't very hard to write an Ltac "is_ctor" tactic.
> > This way might not even be considered too kludgey:
>
> Nice tactic!
> But it doesn't work on sufficiently dependent types; [is_ctor @eq_refl]
> fails with an "illegal application" error.

Oops - that's because destruct isn't a universal tactic for inductive 
types.  Maybe I can use case_eq instead?  Unless that also has issues 
with some inductive types...

-- Jonathan