| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Restore CI with `finmap master`
|
|
Following merge of math-comp/finmap#36
|
|
Fix compatibility for #237
|
|
- reprove rather than specialize `Some_inj` to allow for redefinition
of `nonPropType` in `mathcomp.ssreflect.ssreflect`
- retarget finmap CI to coq-9995-compatibility
|
|
Generalise use of `{pred T}` from coq/coq#9995
|
|
Appears to be needed fo v8.7 compatibility, to avert some bug in early
`only printing` implementation whose fix was not back ported.
|
|
Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).
|
|
Cleaning Require and Require Imports
|
|
|
|
remove deprecated use of `if ... return`
|
|
Replace improper use of non-dependent `return` clause in `if` with a
type cast; an upcoming coq-side PR will discontinue support for this,
in order to support dependent return clauses with an implicit `as`
annotation.
|
|
Remove unused `Require`s and a hint directive from interval.v
|
|
|
|
ssrnum doesn't use zmodp theory
|
|
|
|
[ci] Extend the test-suite
|
|
Refactor CI with separate deploy jobs
|
|
- coq-mathcomp-odd-order.dev + coq.dev
- coq-mathcomp-bigenough.dev, coq-{8.7, 8.8, 8.9, dev}
- coq-mathcomp-finmap.dev, coq-{8.7, 8.8, 8.9, dev}
The configs below are commented-out as the upstream repos' opam is not
yet marked as compatible with mathcomp.dev (and Travis CI doesn't test
it with mathcomp-dev images)
# - coq-mathcomp-real-closed.dev, coq-{8.7, 8.8, 8.9, dev}
# - coq-mathcomp-analysis.dev, coq-{8.8, 8.9, dev}
Close math-comp/math-comp#245
|
|
|
|
|
|
so the images:
- mathcomp/mathcomp-dev:coq-8.7
- mathcomp/mathcomp-dev:coq-8.8
- mathcomp/mathcomp-dev:coq-8.9
- mathcomp/mathcomp-dev:coq-dev
will be pushed to Docker Hub even if a third-party library CI fails.
|
|
|
|
* The latter template job is trusted and only runs:
- in branch master,
- if all build *and* test jobs were successful
(major change in the deployment's condition)
* The other jobs are not tagged with "environment: name: deployment",
so they won't be able to read scoped protected variables.
* href: https://gitlab.com/help/ci/variables/README.md#limiting-environment-scopes-of-variables-premium
|
|
|
|
switching to opam 2.0 format
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Least common childen
|
