test-suite/bugs/closed/2251.v


1
2
3
4
5
6

(* Check that rewrite does not apply to single evars *)

Lemma evar_rewrite : (forall a : nat, a = 0 -> True) -> True.
intros; eapply H.  (* goal is  ?30 = nil  *)
Fail rewrite plus_n_Sm.
Abort.