From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- test-suite/success/unfold.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'test-suite/success/unfold.v') diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 47ca0836..5649e2f7 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -13,3 +13,11 @@ Goal EQ nat 0 0. Hint Unfold EQ. auto. Qed. + +(* Check regular failure when statically existing ref does not exist + any longer at run time *) + +Goal let x := 0 in True. +intro x. +Fail (clear x; unfold x). +Abort. -- cgit v1.2.3