aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-31removing dead code + reshuffling stuffCyril Cohen
2018-07-31Rework the whole Makefile architectureCyril Cohen
- 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
2018-07-27Merge pull request #205 from anton-trunov/ssrnat-addnBAC-lemmaCyril Cohen
Add addnBAC lemma to ssrnat
2018-07-24Add addnBAC, addnBCA, and addnABC lemmas to ssrnatAnton Trunov
Proofs by Cyril Cohen
2018-07-19Merge pull request #202 from CohenCyril/improving-polyLaurent Théry
small generalizations and extensions in poly
2018-07-19last_eq for exhaustivityCyril Cohen
2018-07-19poly_size_eq1 phrased with reflect + combinatorsCyril Cohen
2018-07-19Merge pull request #204 from pi8027/replace-coinductive-with-variantCyril Cohen
Replace all the CoInductives with Variants
2018-07-14updated proposition for big_prod_seq_eq1Cyril Cohen
2018-07-14Laurent's simplificationsCyril Cohen
2018-07-12Replace all the CoInductives with VariantsKazuhiko Sakaguchi
2018-07-04small generalizations in polyCyril Cohen
2018-07-02fix URL in READMEEnrico
Fix #200
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-25 22:25:12 +0000