1 2 3 4 5 6 7 8
(* To shorten interactive scripts, it is better that Try catches non-existent names in Unfold [cf bug #263] *) Lemma lem1 : True. try unfold i_dont_exist in |- *. trivial. Qed.