| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
dev/doc/changes.
|
|
|
|
|
|
After `Drop`, `Coqtop.drop_last_doc` will contain the current document
used by `Coqloop`. This is useful for people wanting to restart Coq
after a `Drop`.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|
|
|
|
|
This follows the merge of AbsInt/CompCert#191.
|
|
just Iris
|
|
|
|
|
|
|
|
|
|
|
|
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
See also GeoCoq/GeoCoq#7.
|
|
|
|
|
|
|
|
|
|
|
|
expected.
|
|
It seems that reinstalling gcc can leave Cygwin in a strange state,
where invocations of gcc fail suddenly. I haven't figure out exactly
why, but this seems to fix it.
|
|
|
|
|
|
|
|
|
|
|
|
top of the linking chain.
|
|
|
|
- timing needs time and python
- check for compiled files without source looks in the install
directory (except for make -f Makefile.ci which doesn't check), as
such the install directory has been renamed to _install_ci and isn't
searched.
|
