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/ltac.v | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'test-suite/success/ltac.v') diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index dfa41c82..02618c2c 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -243,3 +243,35 @@ test_open_match (forall z y, y + z = 0). reflexivity. apply 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. + +(* Do not consider evars as unification holes in Ltac matching (and at + least not as holes unrelated to the original evars) + [Example adapted from Ynot code] + *) + +Ltac not_eq e1 e2 := + match e1 with + | e2 => fail 1 + | _ => idtac + end. + +Goal True. +evar(foo:nat). +let evval := eval compute in foo in not_eq evval 1. +let evval := eval compute in foo in not_eq 1 evval. +Abort. -- cgit v1.2.3