Rodolphe Lepigre

Results 64 comments of Rodolphe Lepigre

> What is your `Declare ML Module` ? I have several plugins, and hence several `Declare ML Module`. They are all placed in the same opam package. So for each...

Yes, on Coq 8.16.0. I'm not sure what the name of the generated `META` file is. How do I figure that out? I expected I could just look in the...

Oh sorry. The error I get is something like: ``` Error: File unavailable: /absolute/path/to/_build/install/default/lib/my_plugins/META ``` I'll try out the MR later and let you know. Thanks!

@ejgallego I confirmed that your patch to Coq (or rather, my back-ported version of it) fixes my problem. Thanks! For reference, see https://github.com/coq/coq/pull/16664.