| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
Simplify the newring hack
|
|
|
|
|
|
|
|
Primary maintainers should be responsive.
[ci skip]
|
|
|
|
We address the easy ones, but they should probably be all removed.
|
|
|
|
|
|
|
|
|
|
global env
|
|
|
|
We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.
Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.
|
|
Caused by a semantic conflict with the separate toplevels PR.
|
|
|
|
|
|
comments.
[ci skip]
|
|
[ci skip]
|
|
Clarification prompted by Jim Fehrle.
[ci skip]
|
|
in CArray
|
|
spawn timeout.
|
|
|
|
The `ide` folder contains two different binaries, the language server
`coqidetop` and `coqide` itself.
Even if these binaries are in the same folder, the only thing they
have in common is that they link to the protocol files. In the OCaml
world, having "doubly" linked files in the same project is considered
a bit of an ugly practice, and some build tools such as Dune disallow it.q
Thus, to clean up the build, we move the common protocol files to its
own library `ideprotocol`.
This helps towards Dune integration and towards having an IDE
standalone target, such as the one that was implemented here:
https://github.com/ejgallego/coqide-exp
|
|
|
|
|
|
instances
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This follows the model of smartmap and smartmap2.
|
|
|
|
|
|
|
|
As per PR comment suggestion
|
