The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Tue, 6 Dec 2011 10:35:35 +0100, Gert Smolka 
<smolka AT ps.uni-saarland.de>
 wrote:
> 1) Why does the induction tactic reject star_ind'?
> 2) Is there a good reason that Coq generates star_ind rather than
>     star_ind'?

The answer may simply be that nobody has asked. At least for the second,
though, there is the issue of consistency and compatability. But it seem
reasonable request to have the first, and an option for the second.

You should file a bug report.

  Tom