summaryrefslogtreecommitdiff
path: root/test-suite/success/Try.v
blob: b356f277c3d4d022faf1d203e4c436d40c4f7f04 (plain)
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.