aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_9453.v
blob: 18745533b20124942bd200c3c8165a0d08ee6c43 (plain)
1
2
3
4
5
6
7
(* check compatibility with 8.8 and earlier for lack of warnings on the nat 5000 *)
Set Warnings Append "+large-nat,+abstract-large-number".
Fail Check 5001.
Check 5000.
(* Error:
To avoid stack overflow, large numbers in nat are interpreted as applications of
Nat.of_uint. *)