| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
interning phase
|
|
|
|
pattern variables
|
|
|
|
|
|
in refman.
|
|
|
|
Hopefully we will re-enable it back soon, I am preparing a refactoring
that should make it more robust w.r.t paths and changes on Windows
which will enable to use a faster build system.
But now it is timing out 100% of the times [due to #8655] so it is not
useful.
|
|
|
|
|
|
|
|
The checks were unnecessarily restrictive (since names can be used for
documentation purposes), and the error message was a bit wrong (it
mentioned a restriction on the explicit status of arguments).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
As reported in #9060, the STM does not handle such constructions
properly. They are anyway fragile, for example Guarded reports a failure
if run at the end of the scripts, so this patch is an improvement.
|
|
|
|
|
|
|
|
comments.
|
|
|
|
which is in lib.cma
|
|
|
|
|
|
|
|
Follow-up of #8987.
|
|
|
|
|
|
|
|
|
|
Improve debug output
|
|
|
|
|
|
This is a required step in order to be able to call `coqdoc` an
generate the documentation of the stdlib, and also useful for other
uses such as the asynchronous engine.
|
|
the same line
|
|
|
|
|
|
in `lib
|
|
|
|
|
|
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
This is what the native Dune Coq version already does, but it is a
problem for Coq Dune too as noted by @vgbl.
|
|
|
|
|
