| Age | Commit message (Collapse) | Author |
|---|
|
Thanks!
|
|
|
|
Fix a typo: `ring_core_scope`
|
|
|
|
|
|
Merge only after solving issue https://github.com/math-comp/math-comp/issues/361
|
|
[ci] fix .gitlab-ci.yml regarding "GIT_STRATEGY: none"
|
|
This could explain why the change in b8eadb8603b83c053a313b39c2a8f268385d8942
was not taken into account.
|
|
[ci] a few improvements of the GitLab CI setup
|
|
* Normal builds (branches & GitHub PRs) are not impacted
* Triggering a scheduled pipeline will only run {coq-dev, mathcomp-dev:coq-dev}
to build and deploy the corresponding image to mathcomp/mathcomp-dev:coq-dev.
* href: https://docs.gitlab.com/ce/user/project/pipelines/schedules.html
|
|
* Add {fourcolor, odd-order} test builds with latest Coq release (8.9)
* As a result, the math-comp CI config w.r.t. {fourcolor, odd-order}
will be similar to that of the upstream repos:
- https://github.com/math-comp/fourcolor/blob/master/.travis.yml
- https://github.com/math-comp/odd-order/pull/16
|
|
* Set "GIT_STRATEGY: none" accordingly
|
|
|
|
totient for prime
|
|
|
|
|
|
docs: Add missing entry in CHANGELOG.md regarding #292
|
|
href: math-comp/math-comp#292
|
|
Reimplement the hierarchy related tools in OCaml
|
|
Fixpoint theorems in finset
|
|
|
|
Remove support for Travis CI (mathcomp switched to Gitlab CI)
|
|
|
|
Mathcomp switched to Gitlab CI via coqbot, see here:
https://github.com/math-comp/math-comp/pull/353#issuecomment-497017174
|
|
|
|
PR template
|
|
|
|
|
|
|
|
|
|
|
|
Also changed eqsVneq.
|
|
Addressing a suggestion by @CohenCyril
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
refactor `seq` permutation theory
|
|
- Change the naming of permutation lemmas so they conform to a
consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`)
prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq`
using a property when there is also a lemma _using_ `perm_eq` for the
same property. Lemmas that do not concern `perm_eq` do _not_ have
`perm` in their name.
- Change the definition of `permutations` for a time- and space-
back-to-front generation algorithm.
- Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and
`tally_seq`, used by the improved `permutation` algorithm.
- add deprecated aliases for renamed lemmas
|
|
remove dependence on Arith lemmas
|
|
|
|
add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma names
|
|
- add notation support for lemma renaming PRs, helping clients adjust
to the name change by emitting warning or raising errors when the old
name is used. The default is to emit warnings, but clients can change
this to silence (if electing to delay migration) or errors (to help
with actual migration). Usage:
Notation old_id := (deprecate old_id new_id) (only parsing).
—> Caveat 1: only prenex maximal implicit of `new_id` are preserved, so,
as `Notation` does not support on-demand implicits, the latter should
be added explicitly as in `(deprecate old new _ _)`.
—> Caveat 2: the warnings are emitted by a tactic-in-term, which
is interpreted during type elaboration. As the SSReflect elaborator may
re-infer type in arguments multiple times (notably, views and arguments
to `apply` and `rewrite`), clients may see duplicate warnings.
- use the `deprecate` facility to introduce the first part of the
refactoring of `seq` permutation lemmas : only lemmas concerning
`perm_eq` should have `perm` as a component of their name.
- document local additions in `ssreflect.v` and `ssrbool.v`
- add 8.8 `odd-order` regression
- the explicit beta-redex idiom use in the `perm_uniq` and
`leq_min_perm` aliases avoids a strange name-sensitive bug of view
interpretation in Coq 8.7.
|
|
|
|
The functionalities of the structure hierarchy related tools `hierarchy-diagram`
and `hierarchy_test.py` are provided by an OCaml script `hierarchy.ml`.
`test_suite/hierarchy_test.v` is deleted. Now make can generate it.
|
