| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-03-13 | Reflection lemmas for `seq.uniq` | 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 | Compatiblity with Ltac as a plugin. | Maxime Dénès | |
| 2017-02-07 | remove documentation for subfilter. | Tanaka Akira | |
| subfilter was exist at ssreflect-1.1 and removed at ssreflect-1.2. | |||
| 2016-12-20 | correct a typo in the documentation | Yves Bertot | |
| 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-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 | 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-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 | Refactoring of binonial | thery | |
| Variable renaming from 'C(m,n) to 'C(n,m) Renaming theorem mul_Sm_binn to mul_bin_diag Adding theorems mul_bin_left mul_bin_right | |||
| 2016-09-16 | Fix compilation after change in CErrors API. | Pierre-Marie Pédrot | |
| 2016-09-07 | fix comment | Enrico | |
| 2016-09-07 | abstract_context utility lemma | Enrico | |
| 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 | |||
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |