diff options
| author | Hugo Herbelin | 2014-11-18 10:18:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-18 10:26:21 +0100 |
| commit | 2e3ae20fe1ed3d7238286720c302bc892505caae (patch) | |
| tree | 74fbaa4ee461bb19b1a349c43c3d2d82dc9005a4 /test-suite | |
| parent | 8d26a1d9a3846c6cbe92a9b2f17ffac6fd7d48f5 (diff) | |
Fixing a little bug with nested but convertible occurrences in "destruct at".
Diffstat (limited to 'test-suite')
| -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 56cdf18e68..277e3ca60a 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. |