| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-02-21 | Compatiblity with Ltac as a plugin. | Maxime Dénès | |
| 2017-02-04 | adding rquot_comRingType | Cyril Cohen | |
| 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 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-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 | 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-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-20 | [field] Remove unnecessary `Program Definition` | Emilio Jesus Gallego Arias | |
| Simple `Definition` should work fine here. This avoids the problem: `Error: Library Coq.Program.Tactics has to be required first.` in math-comp versions that depends on a minimal (or no) Coq stdlib. Tested on 8.5/8.6 | |||
| 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-25 | Factor theorem for decidable fields, (inspired by PY Strub) | Cyril Cohen | |
| 2016-08-25 | Enriched numClosedFieldType so that it factors a lot of theory from both ↵ | Cyril Cohen | |
| complex and algC. The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory have been moved to the numClosedFieldType structure in ssrnum. This covers boths the uses in algC and complex.v. To that end the numClosedFieldType structure has been enriched with conjugation and 'i. Note that 'i can be deduced from the property of algebraic closure and is only here to let the user chose which definitional equality should hold on 'i. Same thing for conjC that could be written `|x|^+2/x, the only nontrivial (up to my knowledge) property is the fact that conjugation is a ring morphism. | |||
| 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 | |
| 2016-07-01 | Fix compilation after renaming of reduction functions and flags in Coq. | Maxime Dénès | |
| 2016-06-17 | fix parsing (coq trunk goal selector/ltac:) | Enrico Tassi | |
| 2016-06-17 | this test is now in Coq, removing it. | Enrico Tassi | |
| 2016-06-16 | Port build system to trunk (ssrmatching merged in Coq) | Enrico Tassi | |
| 2016-06-03 | fixing compilation (with Coq trunk & Coq v8.5) | Matej Kosik | |
| 2016-05-31 | Compatibility with latest Coq trunk. | Emilio Jesus Gallego Arias | |
| 2016-05-18 | Fix compilation after the change of API in Tactics. | Pierre-Marie Pédrot | |
| 2016-05-16 | Fix compilation after the renaming of Lexer into CLexer. | Pierre-Marie Pédrot | |
| 2016-05-12 | Merge pull request #43 from hivert/fixdoc | Georges Gonthier | |
| Fixes the doc of mxrepresentation.v | |||
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |