Ali Caglayan (Oct 08 2021 at 12:28): Ali Caglayan (Oct 08 2021 at 12:28):What is going on here:
https://github.com/coq/coq/pull/15000/checks?check_run_id=3838330986
Pierre-Marie Pédrot (Oct 08 2021 at 12:30):Looks like an OCaml bug?
Gaëtan Gilbert (Oct 08 2021 at 12:35):https://github.com/ocaml/ocaml/issues/10027
Pierre-Marie Pédrot (Oct 08 2021 at 12:39):Coq: the only in-depth user of the worst parts of the OCaml type system out there
Guillaume Melquiond (Oct 08 2021 at 12:43):So, we have exception definitions that use inline records? Was someone really concerned about the cost of OCaml exceptions?
Gaëtan Gilbert (Oct 08 2021 at 12:59):inline records aren't about cost, they're about being able to give names to the fields without having to do some
type contents_of_foo = ...
... of contents_of_foo
boilerplate
Pierre-Marie Pédrot (Oct 08 2021 at 13:04):Bah, it's not useful for exceptions since most of the time there is only one single client destructing the record, i.e. the printer
Last updated: Apr 20 2024 at 06:02 UTC