The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 19 Dec 2012 12:36:09 -0500,
Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> 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

The answer is that it is because "rew" already exists as a tactic
notation, and this notation is of higher priority than simple
identifiers. I did not check it, but it seems reasonnable.

Imagine, you define
Notation "f o g" := (fun x => f (g x)) (at level 0).

Then how should "fun (o:Type) (g:o) (f:forall T, T->Type) => f o g"?

It is not the same thing as hiding an identifier like in "let x := … in
let x := … in …".