Rodolphe Lepigre
Rodolphe Lepigre
We will need to handle dependencies separately to make things work for the editor mode (or rather, LSP server) developed by @ejgallego. In particular, we need to change the way...
## Desired Behavior Cram tests where Coq code is built (with dune) against a coq theory from a local package (explicit dependency being given) fails by not finding the library....
A similar example works for OCaml (see working code in https://github.com/ocaml/dune/pull/6011), so this should probably also work for Coq to give us reasonable cram test support. Such tests are probably...
## Expected Behavior Running `dune build @uselib` should always fail. ## Actual Behavior Running `dune build` (building the OCaml library) first allows `dune build @uselib` to succeed. ## Reproduction -...
OCaml library dependency is not enforced, and it can be used from cram test provided it is built.
The command `dune-release publish distrib` weirdly fails for me (on https://github.com/patoline/patoline), with a seemingly invalid value for `user` and `repo` (referring to the source code variable names). ```bash # dune-release...
After updating `elpi.1.15.2` and `coq-elpi.1.14.0` (under `coq.8.15.1`) to `elpi.1.16.5` and `coq-elpi.1.15.6` (under `coq.8.16.0`) respectively, I noticed a change of behaviour on what a new `Elpi Command` receives on a definition...
This also exposes the `Tac2core.get_map` function, without which it is not possible to add new `set/map` functions from a plugin. - [x] Added / updated **test-suite**. - [x] Added **changelog**.
TODO: - [ ] `to_constr` may miss `unblock`/`block` because of the shortcuts for identity substitutions/liftings. It calls `Vars.subst_instance_constr` which doesn't have any code for finding our primitives. Version 2 (new)...