| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
Seq refactoring; adding `permutations`, extending `allpairs`
|
|
Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an
intermediate file for `hierarchy_test.py`. So the typical usage is:
$ python3.5 etc/utils/hierarchy_test.py \
<(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \
> mathcomp/test_suite/hierarchy_test.v
|
|
- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet
in #299 (except the link to the coq lib `Permutation` predicate).
Use insertions to construct permutations. This definition is closer
to the one proposed by @MrSet, than one using rotations (it adds one
line to the definition of `permutations` but the proofs become a
little simpler.)
- Added support for casts on `map` comprehension general terms.
- Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with
equational proofs; changed `allpairs_comp` to its converse
`map_allpairs` for consistency.
- Add three `allpairs` extensionality lemmas: for the non-localised,
dependent localised and non-dependent localised cases; as per
`eq_in_map`, the latter two are equivalences.
- Documented the `all2` predicate added in #224, and the view
combinators added in #202.
- Renamed `seq2_ind` to `seq_ind2`, and weakened the induction
hypothesis, adding a `size` equality assumption.
- Corrected the header to use `<=>` for `bool` predicate
documentation, and `<->` for `Prop` predicates, following the
library’s general convention.
- Replaced the `nosimpl` in `rev` with a `Arguments simpl never`
directive, making it possible to merge the `Rev` section into the
main `Sequences` section.
- Miscellaneous improvements to proof scripts and file organisation.
- Correct maximal implicits of `constant`.
- Fixes omitted `Prenex Implicit` declaration.
- Other implicits fixes.
- Fix apparent `done` regression It appears `done` now does a weaker
form of intros, and this broke the `dtuple_onP` proof. Updated the
proof to eliminate the issue.
(Commit log edited by @CohenCyril during the squash.)
|
|
|
|
|
|
|
|
|
|
remove support for Coq 8.6
|
|
|
|
rename test-suite -> test_suite to make coq happy
|
|
|
|
Fix inheritances from countalg to finalg
|
|
|
|
|
|
|
|
|
|
Dependent positive finfun
|
|
Describe extension and warn about incompatibilities.
|
|
Line 426 in `integral.v` diverged to over 40 minutes with the new
`finfun.v`, because matching `mod_Iirr` to `quo_Iirr` goes into
exponential backtracking. This is currently averted by limiting the
repetition of `mod_IirrE` in this `rewrite` line.
Making `finfun` mixing opaque brings this down to 40 seconds, and
locking `cfIirr` to a tractable 0.15 seconds, hopefully improving the
instances. This line also takes 47 seconds to execute in the master
branch, so this is likely an undetected Coq performance regression.
|
