| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
In particular, don't use the GitHub interface. Also, not all reviews are
mandatory in some corner cases.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
We make GitHub assign only principal maintainers as reviewers. This
reduces the level of noise (PRs with 10 code owners), and makes it easy
for the assignee to check if all reviews have been completed (all
reviewers in the list have to approve the PR, which was not the case
before if two reviewers were assigned for the same component).
This change means that when a principal maintainer submits a patch
touching the component they own, they should ask a review from the
secondary maintainer.
|
| | |
|
| | |
|
| |\
| |
| |
| | |
get_lexer_state.
|
| | | |
|
| |/
|
|
|
|
|
|
|
| |
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
| |\ |
|
| | |
| |
| |
| | |
longer use camlp4.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
We allow to provide a Coq load path at document creation time. This is
natural as the document naming process is sensible to a particular
load path, thus clarifying this API point.
The changes are minimal, as #6663 did most of the work here. The only
point of interest is that we have split the initial load path into two
components:
- a ML-only load path that is used to locate "plugable" toplevels.
- the normal loadpath that includes `theories` and `user-contrib`,
command line options, etc...
|
| |\ |
|
| | | |
|
| |\ \
| |/
|/| |
|
| | |
| |
| |
| | |
Debian stable version is 0.42-3 right now.
|
| |\ \
| |/
|/|
| | |
Cygwin/Windows
|
| | |
| |
| |
| | |
Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
|
| | |
| |
| |
| |
| | |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| | |
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
|
| |\ \
| |/
|/| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
| | | |
|
| |/
|
|
|
| |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| |
|
|
|
| |
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
|
| | |
|
| | |
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
dev/doc/changes.
|
| |\ \ \ |
|
| | |_|/
|/| | |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
| | | |
|
| | | |
|
| |/ |
|
| |
|
|
|
|
|
|
|
| |
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
| | |
|
| | |
|
| | |
|
| |\
| |
| |
| | |
top of the linking chain.
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | | |/
| |/|
| | |
| | | |
linking chain.
|
| | | | |
|
| |/ /
| |
| | |
With a minimal diff (so I'm not putting quotes ` ` around all the code).
|
| |/
|
|
|
| |
And remove old French part.
And move part about the plugin API to the right section.
|
| |\ |
|
Maxime Dénès
Enrico Tassi
Jim Fehrle
Emilio Jesus Gallego Arias
Théo Zimmermann
Gaëtan Gilbert
Paul Steckler
Hugo Herbelin