rewrite generates ill-typed terms

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2061
From: @fajb
Reported version: 8.2
CC: @mattam82

[coqbot]

Comment author: @fajb

Hello,

In 8.2, the rewrite tactics rewrites recklessly and eventually is responsible for ill-typed terms.

For instance,

Require Import ZArith.

Lemma Zopp2 : forall a : Z, Zopp (Zopp a) = a.
Proof. destruct a ; reflexivity. Qed.

Lemma bug : forall (b:nat), b=0 -> True.
Proof.
intros b H.
rewrite <- Zopp2 in H. (* rewrite does not complain!!! )
auto.
Qed. ( Game over *)
Error: Illegal application (Type Error):
<...>

--
Frédéric

[coqbot]

Comment author: @mattam82

Interestingly enough, this only happens for [rewrite in], not [rewrite] in the goal.

[coqbot]

Comment author: @mattam82

NOW it's assigned to me.

[coqbot]

Comment author: @mattam82

Fixed in the trunk, now rewrite complains that it can't find a well-typed predicate to use.