path: root/test-suite/bugs/closed/shouldfail/2251.v

(* 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  *)
rewrite plus_n_Sm.