diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index fc40ea964f..4a7657e292 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -93,3 +93,20 @@ Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0. intros. destruct (g _). (* This was failing in at least r14571 *) Abort. + +(* Check that subterm selection does not solve existing evars *) + +Goal exists x, S x = S 0. +eexists. +Fail destruct (S _). (* Incompatible occurrences *) +Abort. + +Goal exists x, S 0 = S x. +eexists. +Fail destruct (S _). (* Incompatible occurrences *) +Abort. + +Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. +do 2 eexists. +Fail destruct (_, S _). (* Was succeeding at some time in trunk *) +Show Proof. |