Emilio Jesús Gallego Arias
Emilio Jesús Gallego Arias
This PR provides preliminary support for building math-comp with Dune [support in Dune's master currently] As of today we do consider math-comp as a monolithic library due to Dune's Coq...
Dune support
Hi folks, the Coq mode for Dune is getting more mature, and a big blocker now is integration with Proof General. I am unsure how to best approach this; basically...
Dear PG devs, the topic of how Proof General interacts with Coq has been again discussed Coq upstream. I think the moment has come where we should try to add...
Dear PG devs, it would be great if proofgeneral coq could support ssreflect's style indentation. In order to maximize horizontal proof space, the ssreflect library uses a more conservative indentation,...
Hi folks, as noted by @JasonGross in https://coq.inria.fr/bugs/show_bug.cgi?id=5564 , upstream changes broke again PG's goal display in Coq. This is due to our decision to make all sentences part of...
It is not a secret that emacs default keybindings can cause serious problems to users; IMHO Proof General is not an exception and the default `C-c C-n` can create serious...
There is an issue with the column offsets that are reported in diagnostics, the LSP specification mandates that columns should refer to UTF-16 points, however ocaml-lsp is reporting positions from...
It would be convenient to have the possibility to run the test-suite when building the packages, this can be achieved with `opam -t` provided the packages support it [for Coq...
Hi folks, this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also...