Investigate supporting inlined records for the transparent-types feature

coq-community / coqffi

Automatically generates Coq FFI bindings to OCaml libraries [maintainer=@lthms]

https://coq-community.org/coqffi/

MIT License

35 stars 8 forks source link

Investigate supporting inlined records for the transparent-types feature #70

Open lthms opened 3 years ago

lthms commented 3 years ago

I suspect this is not possible, as I discussed in the commit message of 0f7cb660801f90fe055e9359058023f607afecec

Also, inlined records, that type of the form

    type u = U of { foo : bar }

are still not supported, and might never be supported due to the
restriction of OCaml regarding these types (embodied by the error
message “This form is not allowed as the type of the inlined record
could escape”).