induction with eqn: gives an undocumented (and wrong!) error message

[JasonGross]

Version

8.7.1

Description of the problem

Goal True /\ True -> True.
  intro H.
  induction H eqn:H'. (* Error: a is used in conclusion. *)

The issue here is that the term that induction H eqn:H' builds contains an illegal elimination of a propositional type into Type; this is seen by noticing that the error goes away if /\ is changed to *. I have no strong opinion on whether or not induction should support eqn: on propositional hypotheses (my weak opinion is that it should), but it should definitely not be giving these misleading error messages, and the error message that it gives, whatever it is, should be documented.