| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
They probably don't need to be executable
|
|
Explain into the release process how to prepare the release notes.
|
|
Ack-by: ejgallego
Reviewed-by: vbgl
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: vbgl
Reviewed-by: SkySkimmer
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
proof data on top of declare.
Reviewed-by: ppedrot
|
|
|
|
top of declare.
This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.
This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.
This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.
A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.
Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
|
|
We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.
We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.
cc: #7560
|
|
Reviewed-by: SkySkimmer
|
|
We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.
Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.
Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.
I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.
|
|
TLC and CPDT are not actually tested. No point in keeping them as if they were.
|
|
Reviewed-by: ejgallego
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
|
|
|
We update the URLs to the new ones, even if the previous continue to work.
|
|
|
|
|
|
Ack-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: jfehrle
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82
|
|
We only want stdout, so if there's something in stderr it will both
make a wrong output and make it harder to debug.
|
|
|
|
|
|
|
|
|
|
|
|
the windows crash)
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
This is almost a full rewrite of the contributing guide. The goal was
to have a more structured, and more exhaustive guide, where all our
processes are documented, and from which all the useful documentation
is linked to.
The document lists contribution types in the order in which it is most
natural to go through them: from contributions to the ecosystem, to
issues, to code contributions, to taking part in the maintenance.
However, it seemed important to not neglect this last part if we want
to ease the onboarding of new maintainers (and not just of occasional
contributors).
A table of content makes it easy to go through the document (which is
too long to be read from begin to end).
The guide documents our processes in the way they are today, without
changing anything, but this should be a good basis to make them evolve
in the future. Insufficiently documented tools and processes are
mentioned as such.
|
