| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-17 | .gitignore (ssrmatching.v) | Pierre-Yves Strub | |
| 2017-03-13 | Merge pull request #114 from strub/ignore-vio | Enrico | |
| [gitignore]: ignore .vio files | |||
| 2017-03-13 | Reflection lemmas for `seq.uniq` | Pierre-Yves Strub | |
| 2017-03-13 | [gitignore]: ignore .vio files | Pierre-Yves Strub | |
| 2017-02-23 | [safe-string] Allow compilation with -safe-string. | Emilio Jesus Gallego Arias | |
| The first part of changes is easy, we could maybe polish the notation part a bit more. | |||
| 2017-02-21 | Use pp_with as msg_with is being removed upstream. | Emilio Jesus Gallego Arias | |
| 2017-02-21 | Merge pull request #110 from maximedenes/ltac-plugin | Enrico | |
| Compatiblity with Ltac as a plugin. | |||
| 2017-02-21 | Merge pull request #107 from ejgallego/travis+v8.5 | Enrico | |
| [travis] Make v8.5 build again | |||
| 2017-02-21 | Compatiblity with Ltac as a plugin. | Maxime Dénès | |
| 2017-02-07 | [travis] Make v8.5 build again | Emilio Jesus Gallego Arias | |
| We also remove PFsection6 from build as it seems to be too close. | |||
| 2017-02-07 | remove documentation for subfilter. | Tanaka Akira | |
| subfilter was exist at ssreflect-1.1 and removed at ssreflect-1.2. | |||
| 2017-02-07 | Merge pull request #105 from ejgallego/travis | Cyril Cohen | |
| [travis] Enable build of 70% of Feith-Thompsom proof | |||
| 2017-02-07 | [travis] Build 70% of FT proof. | Emilio Jesus Gallego Arias | |
| I'm afraid we cannot reliably build more with the 50 minutes timeout. | |||
| 2017-02-07 | [travis] Improve parallelism in build (cf #88) | Emilio Jesus Gallego Arias | |
| 2017-02-06 | Build status in README | Cyril Cohen | |
| 2017-02-06 | Merge pull request #103 from ejgallego/travis | Enrico | |
| [travis] Add initial Travis CI support. | |||
| 2017-02-06 | [travis] Add initial Travis CI support. | Emilio Jesus Gallego Arias | |
| 2017-02-04 | adding rquot_comRingType | Cyril Cohen | |
| 2017-01-18 | Merge pull request #78 from falcondai/patch-1 | Enrico | |
| minor change to the opam install example | |||
| 2016-12-20 | Merge pull request #87 from ybertot/master | Assia Mahboubi | |
| correct a typo in the documentation | |||
| 2016-12-20 | correct a typo in the documentation | Yves Bertot | |
| 2016-12-19 | fix compilation on 8.5 | Enrico Tassi | |
| 2016-12-07 | better test for primitive projections | Enrico Tassi | |
| 2016-12-07 | new test for "rewrite /x" when x is Opaque | Enrico Tassi | |
| 2016-12-06 | backport Coq PR#387 on ssrmatching for Coq v8.5 | Enrico Tassi | |
| 2016-12-06 | add test for unfolding primitive projections | Enrico Tassi | |
| 2016-12-06 | Use Tacred.unfoldn [AllOccurrences..] to work around Coq #5250 | Enrico Tassi | |
| 2016-12-06 | rewrite /primitive_projection is now supported (fix #85) | Enrico Tassi | |
| 2016-11-17 | Merge pull request #82 from hivert/fixdoc | Enrico | |
| Just a trivial typo | |||
| 2016-11-17 | Merge remote-tracking branch 'upstream/master' into fixdoc | Florent Hivert | |
| 2016-11-16 | Fixes the doc of mxalgebra | Florent Hivert | |
| 2016-11-08 | fix compilation on 8.6 and trunk | Enrico Tassi | |
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-10-25 | minor change to the opam install example | Falcon Dai | |
| fix a typo in the example command add `opam repo add coq-released http://coq.inria.fr/opam/released` | |||
| 2016-10-24 | removing the need of bracket to delimit ssrpatternarg | Cyril Cohen | |
| 2016-10-24 | wip shorter proof dec factor theorems | Cyril Cohen | |
| 2016-10-24 | better ltngtP | Cyril Cohen | |
| 2016-10-13 | Make: avoid >> Make, pass args to coq_makefile instead (#77) | Enrico Tassi | |
| 2016-10-13 | Merge pull request #65 from gares/master | Cyril Cohen | |
| abstract_context utility lemma | |||
| 2016-10-13 | Merge pull request #66 from thery/master | Cyril Cohen | |
| Adding theorems in binomial | |||
| 2016-10-12 | Merge pull request #76 from matej-kosik/master | Enrico | |
| changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's "pr_o.cmo" plugin | |||
| 2016-10-12 | changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's ↵ | Matej Kosik | |
| "pr_o.cmo" plugin | |||
| 2016-10-05 | Generalization in the type of contra_eq/contra_neq. | Assia Mahboubi | |
| Thanks B. Grégoire for this suggestion. | |||
| 2016-09-28 | Merge pull request #69 from ejgallego/dont-depend-on-program | Cyril Cohen | |
| [field] Remove unnecessary use of `Program Definition` use | |||
| 2016-09-28 | Merge pull request #73 from erikmd/patch-search | Enrico | |
| Add a typing colon in the output of the Search ssreflect vernacular | |||
| 2016-09-27 | Add a typing colon in the output of the Search ssreflect vernacular. | Erik Martin-Dorel | |
| 2016-09-26 | Merge pull request #72 from ppedrot/partial-fix | Enrico | |
| Fix ML compilation after Ltac refactoring. | |||
| 2016-09-24 | Fix ML compilation after Ltac refactoring. | Pierre-Marie Pédrot | |
| 2016-09-23 | Merge pull request #71 from matej-kosik/master | Enrico | |
| FIX: compilation wrt. commit 9c35248 on Coq trunk branch. | |||
| 2016-09-23 | FIX: compilation wrt. commit 9c35248 on Coq trunk branch. | Matej Kosik | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |