induction unknown declaration

Stream: new members

[Joachim Breitner]

I am (again) trying to use my own induction rules. Oddly,

  induction w using neword.cons_induction,

simply says

unknown declaration 'neword.cons_induction'

although that is certainly a known declaration; tactics like refine find it just fine.

Any quick ideas? (I’ll just use refine manually for now)

[Alex J. Best]

Do you have a #mwe?

[Yakov Pechersky]

"using" needs a fully qualified name. So it's probably something like "free_group.neword.cons_induction"