| Commit message (Collapse) | Author | Age |
|
|
|
|
| |
Instead of having the projection data in the constant data we have it
independently in the environment.
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| |_|_|_|/ /
|/| | | | | |
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
is not set
|
| |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
When creating a scheme for bifinite inductive types, we do not create a
fixpoint.
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|/ /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Building this target installs the files that are used by merlin:
- .merlin files (.merlin);
- bin-annot files (.cmt, .cmti);
- source files (.ml, .mli).
Plug-in developpers can thus work with an “installed” version of Coq.
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| |/ / / / / /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
| |/ / / / / /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
| |_|_|_|/ / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
In locally nameless mode (proof mode) names in the context *must*
be distinct otherwise the term representation makes no sense.
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We eta-expand cofixpoints when needed, so that their call-by-need
evaluation is correctly implemented by VM and native_compute.
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We now have only two notions of environments in the kernel: env and
safe_env.
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
|\ \ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
| | | | | | | | |
|
| |_|_|_|_|/ /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The extension mechanism is specific to metasyntax and vernacinterp,
thus it makes sense to place them next to each other.
We also fix the META entry for the `grammar` camlp5 plugin.
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \
| |_|_|_|/ / / / /
|/| | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
The file `config/Makefile` doesn't exist unless we run `./configure`.
We shouldn't have to run `./configure` to run `make clean`. We now no
longer error in any case if `config/Makefile` doesn't exist; this is
simpler than only not erroring if the target is `clean`.
We also now test this property when building on CI.
This fixes #7542
|
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | | |
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
|