The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

Hi Club,

I'm updating a library that builds on Coq 8.2pl to the 8.4 version. There are
some lemmas like

Lemma some_lema (x: A) (b : B) : C :=

   intros x b; rest of the proof.

Qed.

In 8.4 version this shows the error "No product even after head-reduction"

A solution is to change it to

Lemma some_lema : forall (x : A) (b : B), C :=
   intros x b; rest of the proof.
Qed.

or remove the intros (now they are automatically introduced). But since there are lots of lemma like that, I wonder if there is an easiest solution,

An "Unset Automatic Introduction." would be great :P

Thanks!