diff options
author | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 /test-suite/success/ltac.v | |
parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) |
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'test-suite/success/ltac.v')
-rw-r--r-- | test-suite/success/ltac.v | 32 |
1 files changed, 32 insertions, 0 deletions
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. |