aboutsummaryrefslogtreecommitdiff
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-06-08Update INSTALL.mdEnrico
2018-06-08[INSTALL] document opam --root optionEnrico
2018-06-05Update CONTRIBUTING.mdCyril Cohen
2018-06-05Update CONTRIBUTING.mdCyril Cohen
2018-04-24replacing my local `git root` by a universal commandCyril Cohen
2018-04-24fix opam packager script + dependenciesCyril Cohen
2018-04-24Merge pull request #198 from math-comp/close-changelog-4-releaseCyril Cohen
Close ChangeLog to release 1.7
2018-04-24fix typoEnrico
thanks Yves
2018-04-24Update ChangeLogEnrico
2018-04-24Merge pull request #197 from amahboubi/edit-changesEnrico
Improved ChangeLog
2018-04-24Removed content about files not in the repo/release + minor stuffAssia Mahboubi
2018-04-23Latest changes added to change log.Assia Mahboubi
2018-04-23Improved ChangeLogAssia Mahboubi
One paragraph per version + spell check
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-20update installation instructionsEnrico Tassi
2018-04-20move etc/ files to the root and remove obsolete onesEnrico Tassi
2018-04-20generate the documentation for 1.7Enrico Tassi
2018-04-20travis: build against 8.6 -> 8.8Enrico Tassi
2018-04-20Fix the script that generates the docEnrico Tassi
2018-04-20move the webpage from gh-pages branch to docs/Enrico 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:50:26 +0000