| Age | Commit message (Collapse) | Author |
|---|
|
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...
|
|
... 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.
|
|
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"
```
|
|
|
|
And remove old French part.
And move part about the plugin API to the right section.
|
