diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-05-12 17:41:45 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-05-12 19:10:44 +0200 |
commit | b338af912c32ab87d6668923add72a56408bddf8 (patch) | |
tree | 180408f56d4a1739a0efc9d01828a163e1cd1619 /printing/ppvernac.mli | |
parent | 1f3ea50258490ac8b5a395ac0ff2bca7326e755f (diff) |
List.nth_error directly produces Some/None instead of value/error
List.nth_error and List.hd_error were the only remaining places in
the whole stdlib to use type "Exc" instead of "option" directly.
So let's simplify things and use option everywhere. In particular,
during teaching sessions about lists, we won't have anymore to explain
the (lack of) difference between Exc,value,error and option,Some,None.
This might cause a few incompatibilities in proof scripts, if they
syntactically expect "value" or "error" to occur, but this should
hopefully be very rare and quite easy to fix.
Diffstat (limited to 'printing/ppvernac.mli')
0 files changed, 0 insertions, 0 deletions