| Age | Commit message (Collapse) | Author |
|---|
|
should fix #238
|
|
This reverts commit 044634dcc2f645e3afbdad6cb8dcc66f3eb4a87e.
See issue https://github.com/math-comp/odd-order/pull/5
|
|
fix some bugs in Makefile
|
|
Statement of `bool_irrelevance` more consistent with its name.
|
|
|
|
|
|
- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style
|
|
they are already defined in ssrfun
ChangeLog updated
|
|
[opam]: add dev-repo links
|
|
|
|
This commit fixes the following issue:
```shell
$ opam pin add coq-mathcomp-ssreflect --dev
[ERROR] "dev-repo" field missing in coq-mathcomp-ssreflect metadata,
you'll need to specify the pinning location
```
This commit also changes http to https for the homepage links.
|
|
Added the definition of all2.
This definition of all2 has the useful computational behaviour, and all2E unfolds an equivalent one.
|
|
Tool to prove only P0 -> P1 -> ... -> Pn -> P0
but use any implication Pi -> Pj
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Cleanup, refactoring and generalize the makefile architecture
- Reuses @strub math-comp/analysis Makefile / Makefile.common organization
- As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable
|
|
Proofs by Cyril Cohen
|
|
small generalizations and extensions in poly
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
I had put this for compatibility with mathcomp 1.6 when we were still using svn, but I am afraid it got under the radar.
We should decide
- if we revert the change of `ltngtP`,
- if we document (and extend) the compatibility module
- or if we just remove the module and keep the change to `ltngtP`
I am personally in favour of the last
|
|
|
|
Dear devs, in an attempt to simplify the code of intro patterns we came up with a proposal that:
- simplifies the code of the plugin
- breaks only one line in the entire mathcomp, the one fixed by this patch.
The code we want to simplify is the one deferring clear switches inside an intro pattern.
The implementation is tricky because just delaying the clear switch until the end of the pattern is not enough, for example:
```
move=> {x} /andP[x y].
```
In this case `x` is both cleared and used. In order to be able to use `x`, given that the clear has not been performed yet, we rename `x` into `_x_` (when `{x}` is executed) so that when `x` is later executed we can use the name `x`, and then `.` is executed clear `_x_` instead of `x`.
So systematically "always rename now & clear later" seem to be OK, but it is not. The extra complication is that "rename" may break later intro pattern using terms as views. Eg
```
move=> {x} /andP[Ha Hb] /x.
```
What the code does today is:
- when `{x}` is execute look-ahead in the patter and see if `x` is used as a name to be introduced
- if so, "rename"
- otherwise don't rename (just delay)
This way of doing things is not only complicated but also incomplete, Eg
```
move=> {x} /orP[x | /x].
```
would misbehave, since the look-ahead is not "semantic".
Anyway, the proposed behavior is:
- `{x}` always renames now and clears (the renamed) later
- `{clears}/views` is always "compiled" as `/views{clears}` (most of the occurrences in the library are ok with this simpler rule, but for the one fixed in this PR).
- bonus: support `{}/view` (as in `rewrite {}rule`) to signal that the immediately following `view` has to be cleared, that is `{}/v` compiled as `/v{v}`.
What do you think?
```
```
|
|
This was the proof does not depend on the lemma name.
|
|
|
|
This backports the changes from Coq's [PR #6911](https://github.com/coq/coq/pull/6911)
And also fixes a typo in doc comments
|
|
Change deprecated Arguments Scope to Arguments
|
