From bc1ddb1081dd44887cb2f8b33937138cb1e1658c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 11 Sep 2010 19:19:04 +0000
Subject: 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
---
 test-suite/success/ltac.v   | 15 +++++++++++++++
 test-suite/success/unfold.v |  8 ++++++++
 2 files changed, 23 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index bbaeb08992..32c6d14311 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -266,3 +266,18 @@ reflexivity.
 f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *)
 || exact I.
 Qed.
+
+(* Test regular failure when clear/intro breaks soundness of the
+   interpretation of terms in current environment *)
+
+Ltac g y := clear y; assert (y=y).
+Goal forall x:nat, True.
+intro x.
+Fail g x.
+Abort.
+
+Ltac h y := assert (y=y).
+Goal forall x:nat, True.
+intro x.
+Fail clear x; f x.
+Abort.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 47ca0836b5..5649e2f712 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