| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-04 | Merge pull request #1 from ppedrot/econstr | Maxime Dénès | |
| Fix ML compilation after introduction of EInstance. | |||
| 2017-04-04 | Fix ML compilation after introduction of EInstance. | Pierre-Marie Pédrot | |
| 2017-04-03 | Merge pull request #118 from maximedenes/coq-pr417-landing | Enrico | |
| Adapt the ssr plugin to Coq's PR#417. | |||
| 2017-04-03 | Adapt the ssr plugin to Coq's PR#417. | Maxime Dénès | |
| Let-ins in constrexpr and glob_constr now take an optional type, instead of relying on a cast in the body. | |||
| 2017-03-24 | [econstr] Adapt to naming changes. | Emilio Jesus Gallego Arias | |
| 2017-03-24 | Port to EConstr | Enrico Tassi | |
| 2017-03-23 | ssrtest/elim.v: don't depend on Function | Enrico Tassi | |
| We inline the lemmas it generated, to ectly test the same thing as before. | |||
| 2017-03-21 | Merge pull request #108 from ejgallego/pp_new_fix | Maxime Dénès | |
| Use pp_with as msg_with is being removed upstream. | |||
| 2017-03-21 | Merge pull request #111 from ejgallego/safe_string | Enrico | |
| Compile with -safe-string | |||
| 2017-03-17 | Merge pull request #117 from strub/ignore-ssrmatching | Enrico | |
| .gitignore (ssrmatching.v) | |||
| 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 | |||
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |