| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
- make explicit that members of the enforcement team shouldn't be at once
participant in a discussion and moderators;
- try to be more positive by defending a pedagogical approach to address
most violations.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
|
|
We'd like to use `(lang 1.1)` features. Elpi needs update as recent
`ppx_tools_versioned` changes broke it.
|
|
|
|
|
|
error" argument in make
|
|
|
|
|
|
"treat errors as warnings" flag (-W) is applied. "1" or undefined
includes the flag, other values or undefined omit it.
Removed the "-warn-error" parameter to configure. "-profile XXX" will
no longer cause these flags to be used.
|
|
As per https://github.com/coq/coq/pull/8167#issuecomment-416929865
|
|
As per https://github.com/coq/coq/pull/8349#pullrequestreview-150456919
|
|
|
|
|
|
context after "Set Diffs"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This tests the outputs of extraction, to some extent.
|
|
|
|
|
|
This has become mostly garbage since GitLab CI became our main CI platform.
|
|
And fix wrong indentation.
|
|
|
|
There's no need to build dependencies for it.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
