| Age | Commit message (Collapse) | Author |
|---|
|
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
|
|
should fix #238
|
|
- 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
|
|
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.
|
|
|
|
- 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
|
|
|
|
|
|
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?
```
```
|
|
|
|
|
|
|
|
|
|
It was emitting a deprecation warning and will soon be removed from Coq.
|
|
|
|
New packager
|
|
|
|
Fixes #139
|
|
|
|
Simple `Definition` should work fine here.
This avoids the problem:
`Error: Library Coq.Program.Tactics has to be required first.`
in math-comp versions that depends on a minimal (or no) Coq stdlib.
Tested on 8.5/8.6
|
|
complex and algC.
The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory
have been moved to the numClosedFieldType structure in ssrnum.
This covers boths the uses in algC and complex.v. To that end the
numClosedFieldType structure has been enriched with conjugation and 'i.
Note that 'i can be deduced from the property of algebraic closure and is
only here to let the user chose which definitional equality should hold
on 'i. Same thing for conjC that could be written `|x|^+2/x, the only
nontrivial (up to my knowledge) property is the fact that conjugation
is a ring morphism.
|
|
|
|
This reverts commit 006565bdb5b473afff5f834e4b20320bb0a419fd.
since Coq commit c6b75e1b693ab8c7af2efd1b93f04eab248e584c
make this unnecessary
|
|
This shall be reverted, it is there only to make ssr compile on jenkins
and help the release of Coq
|
|
|
|
Two lemmas provide splitting field for a given polynomials, and a finite field
of a given (prime power) order, respectively.
Internal comments document type-checking performance issues that arose.
|
|
|
|
|
|
|
|
|
|
Default cloning requires a manifest field class.
|
|
Type cast on head constant spoils projection registration (Coq misfeature).
|
|
|
|
It's no more crashing but it's still way to long...
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
