| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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.
|
|
We use git check-attr to look at the same files as git diff --check.
|
|
|
|
|
|
|
|
|
|
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.
|
|
The OSX binaries were signed twice with a fake identity, leading to some
obscure errors on Travis in some cases.
We disable code signing for Travis artifacts. For released packages,
a proper signing will be applied manually.
|
|
|
|
|
|
|
|
|
