diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-20 10:25:37 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-20 17:45:22 +0200 |
commit | 513e194656429b6a9142a3a34095cee2c6f8ee96 (patch) | |
tree | a935129d675b538a12102e1cddac453a05f6b76e /test-suite/success/Case13.v | |
parent | 283579ff70d324296e2b7ee2535b1187ca32e0cb (diff) |
Fixing an anomaly in printing a unification error message.
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 f14725a8e..8f95484cf 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. |