diff options
Diffstat (limited to 'test-suite/success/unfold.v')
| -rw-r--r-- | test-suite/success/unfold.v | 8 |
1 files changed, 8 insertions, 0 deletions
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. |