diff options
Diffstat (limited to 'test-suite/success/Case13.v')
-rw-r--r-- | test-suite/success/Case13.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f14725a8..8f95484c 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with | _ => 0 end). +(* This one could eventually be solved, the "Fail" is just to ensure *) +(* that it does not fail with an anomaly, as it did at some time *) +Fail Check (fun x : I' 0 => match x return _ x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). + (* Check insertion of coercions around matched subterm *) Parameter A:Set. |