The Coq mailing list

[Denis Cousineau <cousineau AT lix.polytechnique.fr>]

Dear coq-clubbers,

I've found that the tactic subst  only works with equations in contexts that 
concern variables that were quantified in the goal, and not global parameters.

For example :

(************************************)
Lemma goal : forall a:nat,  a= 42 -> a <= a.
Proof.
intros.
subst.
(************************************)


works (the goal becomes 42 <= 42)

while

(************************************)
Parameter a:nat.

Lemma goal :   a= 42 -> a <= a.
Proof.
intros.
subst.
(************************************)

does not work (the goal is not rewritten into 42 <= 42).

Is this a bug or a feature ?

Does anyone has a hint to bypass this problem ?

Thanks,


--
Denis Cousineau