diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/ltac.v | 15 | ||||
| -rw-r--r-- | test-suite/success/unfold.v | 8 |
2 files changed, 23 insertions, 0 deletions
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. |