diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Case13.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index 06149b3fa..71c9191d6 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -12,16 +12,13 @@ Check [x]Cases x of (C2 n) => O | O => O | (S n) => n end. (* Coercion not at the root of pattern *) Check [x]Cases x of (C2 O) => O | _ => O end. -(* TODO: insert unification inside patterns to get these examples working - +(* Unification and coercions inside patterns *) Check [x:(option nat)]Cases x of None => O | (Some O) => O | _ => O end. -(* Coercion up to delta-conversion *) +(* Coercion up to delta-conversion, and unification *) Coercion somenat := (Some nat). Check [x]Cases x of None => O | O => O | (S n) => n end. -*) - (* Coercions with parameters *) Inductive listn : nat-> Set := niln : (listn O) |