Rodolphe Lepigre
Rodolphe Lepigre
This goes a bit further than #567, but there are still things to figure out: - [ ] Making sure CI still works. - [ ] Figure out whether there...
This used to also be the case for `coq.env.current-path`, but we fixed it in https://github.com/LPCIC/coq-elpi/pull/605. There is no available Coq API that would let us correctly implement `coq.env.current-section-path` at interp...
## Expected Behavior Running `dune coq top --no-build ...` should not fail if there is a concurrently running `dune build` command. ## Actual Behavior You get: `Error: A running dune...
## Desired Behavior Currently, `dynamic_include` cannot deal with files using `subdir`. How hard would it be to support it? ## Example The example I have in mind is simple, and...
Since refactoring `Constr.t` to combine primitive values into an intermediate type is not a clear win (see https://github.com/coq/coq/pull/17951), here is an attempt to add ~~primitive `char` and `string` types by...
These versions are probably obsolete at this point, and this allows simplifying the code slightly.
We could use this data structure to have more precise contexts at a small cost. Not sure we want to do that right now, I think I'd prefer keeping the...
A first step could be to use [this](http://www.schaik.com/pngsuite/) test suite, which is what I originally did (and it is used [here](https://github.com/patoline/patoline/blob/master/examples/imagelib_test.txp)).
File [bug.tar.gz](https://github.com/user-attachments/files/15900849/bug.tar.gz) (updated) contains a small dune project that exhibits an issue related to dynamic linking. It is not clear to me whether the problem lies with dune itself, or...