diff options
author | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /test-suite/success/ltac.v | |
parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) |
Imported Upstream version 8.3upstream/8.3
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. |