diff options
| author | Hugo Herbelin | 2014-08-09 18:53:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:39 +0200 |
| commit | efa1c32a4d17870794dbc6f0301c3c0d46637a55 (patch) | |
| tree | 235cb1903dc5ffdd2ad4bdb7d3bc9cfc58e10de2 /test-suite | |
| parent | 5dcafa956e49eefc451dd021a0fe8ad2e2338088 (diff) | |
Fixing unification of subterms identified by patterns.
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. |