| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-31 | agressive fix for duplicated files! | Cyril Cohen | |
| 2018-07-12 | Replace all the CoInductives with Variants | Kazuhiko Sakaguchi | |
| 2018-04-20 | remove ssr plugin for 8.4 and 8.5 | Enrico Tassi | |
| 2018-03-21 | Declare 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-02-26 | Add ssrmatching.v transitional file | Erik 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 | |||
| 2017-11-14 | Update v8.5 plugin to fix math-comp/math-comp#61 | Erik Martin-Dorel | |
| 2017-10-30 | Fix obsolete vernacular syntax for locality. | Maxime Dénès | |
| It was emitting a deprecation warning and will soon be removed from Coq. | |||
| 2017-06-09 | fix compilation on 8.5 | Enrico Tassi | |
| 2017-06-09 | fix compilation on 8.6 | Enrico Tassi | |
| 2017-06-07 | For trunk, use merged ssr plugin. | Maxime Dénès | |
| 2017-06-06 | Fix plugin after Sigma removal. | Maxime Dénès | |
| 2017-06-06 | Merge pull request #127 from herbelin/trunk+interp_closed_glob_constr | Maxime Dénès | |
| Binding glob_constr to interp_glob_closure so as to factorize low-level code. | |||
| 2017-05-31 | Adapting to PR #590 (a more explicit algebraic type for evars of kind ↵ | Hugo Herbelin | |
| MatchingVar). | |||
| 2017-05-31 | Binding glob_constr to interp_glob_closure so as to factorize low-level code. | Hugo Herbelin | |
| 2017-05-25 | [coqlib] Update to explicitly build terms from references. | Emilio Jesus Gallego Arias | |
| See coq/coq#678 | |||
| 2017-05-25 | Merge pull request #125 from ejgallego/options+remove_non_sync | Maxime Dénès | |
| [options] Sync with upstream API changes. | |||
| 2017-05-23 | [options] Sync with upstream API changes. | Emilio Jesus Gallego Arias | |
| 2017-04-19 | [ast] Adapt to Coq's #402 new generic AST node. | Emilio Jesus Gallego Arias | |
| 2017-04-17 | Coq PR #565: G_vernac.subgoal_command is replaced by query_command | Gaetan Gilbert | |
| 2017-04-12 | Merge pull request #119 from maximedenes/econstr | Maxime Dénès | |
| Econstr support | |||
| 2017-04-07 | [camplX] Remove camlp4 support. | Emilio Jesus Gallego Arias | |
| Adapting to Coq upstream. | |||
| 2017-04-05 | Merge remote-tracking branch 'upstream/master' into econstr | Maxime Dénès | |
| 2017-04-04 | Fix ML compilation after introduction of EInstance. | Pierre-Marie Pédrot | |
| 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-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-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 | Compatiblity with Ltac as a plugin. | Maxime Dénès | |
| 2016-12-19 | fix compilation on 8.5 | Enrico Tassi | |
| 2016-12-06 | backport Coq PR#387 on ssrmatching for Coq v8.5 | 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-08 | fix compilation on 8.6 and trunk | Enrico Tassi | |
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-10-24 | removing the need of bracket to delimit ssrpatternarg | Cyril Cohen | |
| 2016-10-12 | changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's ↵ | Matej Kosik | |
| "pr_o.cmo" plugin | |||
| 2016-09-27 | Add a typing colon in the output of the Search ssreflect vernacular. | Erik Martin-Dorel | |
| 2016-09-24 | Fix ML compilation after Ltac refactoring. | Pierre-Marie Pédrot | |
| 2016-09-23 | FIX: compilation wrt. commit 9c35248 on Coq trunk branch. | Matej Kosik | |
| 2016-09-22 | fix compilation wrt. commit 699b70c in Coq trunk | Matej Kosik | |
| 2016-09-16 | Fix compilation after change in CErrors API. | Pierre-Marie Pédrot | |
| 2016-08-26 | fix compilation wrt. commit 69388fc in Coq trunk | Matej Kosik | |
| 2016-08-25 | FIX: adding missing version of the ssreflect plugin that compiles with Coq v8.6. | Matej Kosik | |
| The committed files represent copies of the ssreflect plugin for Coq trunk taken from commit c353aa5 which is the last commit in which ssreflect plugin marked for Coq trunk is usable with both, Coq trunk as well as Coq v8.6. | |||
| 2016-08-24 | Possible code compaction motivated by Enrico's remark: ↵ | Matej Kosik | |
| https://github.com/math-comp/math-comp/pull/58#discussion_r76048943 | |||
| 2016-08-17 | Removing calls of "Context.Named.Declaration.to_tuple" function | Matej Kosik | |
| 2016-08-17 | use a convenient module alias instead of "Context.Rel.Declaration" and ↵ | Matej Kosik | |
| "Context.Named.Declaration" | |||
| 2016-08-16 | fix compilation on trunk (thanks Matej) | Enrico Tassi | |
| 2016-07-03 | Fix compilation after Errors and Closure were renamed. | Maxime Dénès | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |