The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Can someone explain to me why it matters whether I name a tactic [rew] or [rew'] in the following code (in Coq 8.4):

Goal forall x y z : Type, x = y -> y = z -> x = z.

intros.

let rew' := ( fun H => rewrite H in * ) in

rew' H0.

assumption.

Qed.

(* success *)

Goal forall x y z : Type, x = y -> y = z -> x = z.

intros.

let rew := ( fun H => rewrite H in * ) in

rew H0. (* Error: Library Coq.Setoids.Setoid has to be required first. *)

Abort.

Require Import Setoid.

Goal forall x y z : Type, x = y -> y = z -> x = z.

intros.

let rew := ( fun H => rewrite H in * ) in

rew H0. (* Error: Tactic failure:Nothing to rewrite. *)

Thanks.

-Jason