diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-11 19:19:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-11 19:19:04 +0000 |
| commit | bc1ddb1081dd44887cb2f8b33937138cb1e1658c (patch) | |
| tree | 396f99140c055245ae45cda6afd68462634c0191 /test-suite/success/unfold.v | |
| parent | b0dd26994fcc609668466d969dd88d9a008030e2 (diff) | |
Improving a few error messages in Ltac interpretation
- improving error message when a reference to unfold is not found
- repairing anomaly when an evaluable reference exists at
internalisation-time but not at run time, and similarly for an
arbitrary term (but the latter is new from 8.3 because of the new
use of retyping instead of understand for typing Ltac values)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13408 85f007b7-540e-0410-9357-904b9bb8a0f7
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 47ca0836b..5649e2f71 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. |