aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Collapse)Author
2018-07-14updated proposition for big_prod_seq_eq1Cyril Cohen
2018-07-14Laurent's simplificationsCyril Cohen
2018-07-04small generalizations in polyCyril Cohen
2018-04-24fix opam packager script + dependenciesCyril Cohen
2018-04-20fix symlinks to README, INSTALL and LICENSEEnrico Tassi
2018-04-20remove the attic/ directoryEnrico Tassi
2018-04-20remove ssr plugin for 8.4 and 8.5Enrico Tassi
2018-04-20Fix the script that generates the docEnrico Tassi
2018-04-20remove v8.4 code from MakefileEnrico Tassi
2018-04-20Merge remote-tracking branch 'origin/pr/189'Enrico Tassi
2018-04-20Merge remote-tracking branch 'origin/pr/192'Enrico Tassi
2018-04-20Merge remote-tracking branch 'origin/pr/191'Enrico Tassi
2018-04-20Merge remote-tracking branch 'origin/pr/193'Enrico Tassi
2018-04-18Moving real_closed to another repoCyril Cohen
2018-04-17Removing undocumented compatibility moduleCyril Cohen
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
2018-04-17move odd_order to its own repositoryEnrico Tassi
2018-04-16[separable] put clear switch near viewEnrico
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? ``` ```
2018-04-12ssrnat: don't use `fix n` but rather `fix name n`Enrico Tassi
This was the proof does not depend on the lemma name.
2018-04-12remove ssrtest: it now belongs to CoqEnrico Tassi
2018-03-21Declare prenex implicits for `Some_inj`Anton Trunov
This backports the changes from Coq's [PR #6911](https://github.com/coq/coq/pull/6911) And also fixes a typo in doc comments
2018-03-20Merge pull request #185 from jashug/deprecate-arguments-scopeEnrico
Change deprecated Arguments Scope to Arguments
2018-03-06Merge pull request #178 from thery/masterAssia Mahboubi
generalize the default value of nth in nth_iota
2018-03-04Change deprecated Arguments Scope to ArgumentsJasper Hugunin
2018-03-03Merge pull request #179 from jashug/deprecate-implicit-argumentsEnrico
Remove Implicit Arguments command in favor of Arguments
2018-02-26Add ssrmatching.v transitional fileErik Martin-Dorel
The content of this file is similar to that of ssrfun.v and aims to increase compatibility with Coq 8.6+ for third-party libraries that depend on both math-comp and ssrmatching.v Close #63
2018-02-22Change Implicit Arguments to Arguments in odd_orderJasper Hugunin
2018-02-22Change Implicit Arguments to Arguments in real_closedJasper Hugunin
2018-02-22Change Implicit Arguments to Arguments in characterJasper Hugunin
2018-02-21Change Implicit Arguments to Arguments in fieldJasper Hugunin
2018-02-21Change Implicit Arguments to Arguments in solvableJasper Hugunin
2018-02-21Change Implicit Arguments to Arguments in algebraJasper Hugunin
2018-02-21Change Implicit Arguments to Arguments in fingroupJasper Hugunin
2018-02-21Change Implicit Arguments to Arguments in ssreflectJasper Hugunin
2018-02-21Merge pull request #177 from gares/fix/missing-ssrtest-in-MakeCyril Cohen
add 3 tests to Make
2018-02-16generalize nth_iotathery
2018-02-06add 3 tests to MakeEnrico Tassi
2018-02-06fixing things that @ggonthier and @ybertot spotted and some I spottedCyril Cohen
2018-02-06running semi-automated linting on the whole libraryCyril Cohen
2018-02-05tide up proof of card_inj_ffunsEnrico Tassi
2018-01-26Merge pull request #171 from CohenCyril/mxdirect_deltaCyril Cohen
The spaces generated by some delta_mx are in a direct sum
2017-12-20Merge pull request #172 from CohenCyril/row_mx_eq0Assia Mahboubi
Adding row/col/block_mx_eq0
2017-12-15Merge pull request #170 from CohenCyril/mulr_eq1ECyril Cohen
Using x * y = 1 and x / y = 1 to derive invertibility and the inverse
2017-12-15Merge pull request #157 from ybertot/add-subset-orbit-theoremsCyril Cohen
Adds generalizations of theorems relying on injectivity
2017-12-14Merge pull request #167 from hivert/PR2Cyril Cohen
Resubmitted lemma reshape_index_leq for discussion
2017-12-14Merge pull request #155 from erikmd/fix/gh-61Cyril Cohen
Update v8.5 plugin to fix math-comp/math-comp#61
2017-12-14The spaces generated by some delta_mx are in a direct sumCyril Cohen
proof by @ggonthier
2017-12-14Using x * y = 1 and x / y = 1 to derive the inverseCyril Cohen
fixes #169
2017-12-12Adding row/col/block_mx_eq0Cyril Cohen
2017-12-12refactored proof and renamed to reshape_leq and removed spurious hypothesisCyril Cohen
2017-12-12bigop with allpairsFlorent Hivert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:18:48 +0000