[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: [coqdev] Bytecode/native interoperability of .vo/.coq files



On 22/10/2015 11:55, Stéphane Glondu wrote:
> Does this behaviour ring a bell to someone? Isn't it the symptom of a
> bug somewhere?

Looks like a bug. Coq object files are arch-dependent but should not
vary depending on byte- or native-compilation, as far as I understand.

I am currently looking at the generated files to get where things go
awry. May it be the case that OCaml marshaling itself is sensitive to
the compilation mode ?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature


Reply to: