aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-12Merge pull request #190 from gares/anon-fixEnrico
ssrnat: don't use `fix n` but rather `fix name n`
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-21Merge pull request #187 from anton-trunov/fix-some-inj-to-use-it-as-a-viewAssia Mahboubi
Declare prenex implicits for `Some_inj`
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-06Merge pull request #186 from anton-trunov/add-dev-repo-to-installAssia Mahboubi
[doc] Add instructions for dev version installation via OPAM
2018-03-06[doc] Add instructions for dev version installation via OPAMAnton Trunov
Plus minor formattig tweaks and typo fixes.
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-03-03Merge pull request #180 from erikmd/export-ssrmatchingEnrico
Add ssrmatching.v transitional file
2018-03-03Merge pull request #181 from gares/travis/no85Enrico
travis: disable Coq 8.5
2018-02-27travis: disable Coq 8.5Enrico Tassi
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-06Merge pull request #164 from CohenCyril/lintingCyril Cohen
linting of the whole library
2018-02-06Update README.mdCyril Cohen
fixes #175
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-05Merge pull request #176 from gares/fix/card_inj_ffunsAssia Mahboubi
tide up proof of card_inj_ffuns
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-14Merge pull request #168 from hivert/allpairsCyril Cohen
bigop with allpairs
2017-12-14Using x * y = 1 and x / y = 1 to derive the inverseCyril Cohen
fixes #169
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 19:47:52 +0000