diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/destruct.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 56cdf18e6..277e3ca60 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -113,6 +113,12 @@ destruct (_, S _). (* Was unifying at some time in trunk, now takes the first oc change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n0). Abort. +(* An example with incompatible but convertible occurrences *) + +Goal id (id 0) = 0. +Fail destruct (id _) at 1 2. +Abort. + (* Avoid unnatural selection of a subterm larger than expected *) Goal let g := fun x:nat => x in g (S 0) = 0. |