aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Collapse)Author
2017-04-05Merge remote-tracking branch 'upstream/master' into econstrMaxime Dénès
2017-04-04Fix ML compilation after introduction of EInstance.Pierre-Marie Pédrot
2017-04-03Adapt 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-24Port to EConstrEnrico Tassi
2017-03-23ssrtest/elim.v: don't depend on FunctionEnrico Tassi
We inline the lemmas it generated, to ectly test the same thing as before.
2017-03-21Merge pull request #108 from ejgallego/pp_new_fixMaxime Dénès
Use pp_with as msg_with is being removed upstream.
2017-03-13Reflection 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-21Use pp_with as msg_with is being removed upstream.Emilio Jesus Gallego Arias
2017-02-21Compatiblity with Ltac as a plugin.Maxime Dénès
2017-02-07remove documentation for subfilter.Tanaka Akira
subfilter was exist at ssreflect-1.1 and removed at ssreflect-1.2.
2017-02-04adding rquot_comRingTypeCyril Cohen
2016-12-20correct a typo in the documentationYves Bertot
2016-12-19fix compilation on 8.5Enrico Tassi
2016-12-07better test for primitive projectionsEnrico Tassi
2016-12-07new test for "rewrite /x" when x is OpaqueEnrico Tassi
2016-12-06backport Coq PR#387 on ssrmatching for Coq v8.5Enrico Tassi
2016-12-06add test for unfolding primitive projectionsEnrico Tassi
2016-12-06Use Tacred.unfoldn [AllOccurrences..] to work around Coq #5250Enrico Tassi
2016-12-06rewrite /primitive_projection is now supported (fix #85)Enrico Tassi
2016-11-17Merge remote-tracking branch 'upstream/master' into fixdocFlorent Hivert
2016-11-16Fixes the doc of mxalgebraFlorent Hivert
2016-11-08fix compilation on 8.6 and trunkEnrico Tassi
2016-11-07update copyright bannerAssia Mahboubi
2016-10-24removing the need of bracket to delimit ssrpatternargCyril Cohen
2016-10-24wip shorter proof dec factor theoremsCyril Cohen
2016-10-24better ltngtPCyril Cohen
2016-10-13Make: avoid >> Make, pass args to coq_makefile instead (#77)Enrico Tassi
2016-10-13Merge pull request #65 from gares/masterCyril Cohen
abstract_context utility lemma
2016-10-13Merge pull request #66 from thery/masterCyril Cohen
Adding theorems in binomial
2016-10-12changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's ↵Matej Kosik
"pr_o.cmo" plugin
2016-10-05Generalization in the type of contra_eq/contra_neq.Assia Mahboubi
Thanks B. Grégoire for this suggestion.
2016-09-28Merge pull request #69 from ejgallego/dont-depend-on-programCyril Cohen
[field] Remove unnecessary use of `Program Definition` use
2016-09-27Add a typing colon in the output of the Search ssreflect vernacular.Erik Martin-Dorel
2016-09-24Fix ML compilation after Ltac refactoring.Pierre-Marie Pédrot
2016-09-23FIX: compilation wrt. commit 9c35248 on Coq trunk branch.Matej Kosik
2016-09-22fix compilation wrt. commit 699b70c in Coq trunkMatej 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-16Refactoring of binonialthery
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-16Fix compilation after change in CErrors API.Pierre-Marie Pédrot
2016-09-07fix commentEnrico
2016-09-07abstract_context utility lemmaEnrico
2016-08-26fix compilation wrt. commit 69388fc in Coq trunkMatej Kosik
2016-08-25FIX: 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-25Factor theorem for decidable fields, (inspired by PY Strub)Cyril Cohen
2016-08-25Enriched 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-24Possible code compaction motivated by Enrico's remark: ↵Matej Kosik
https://github.com/math-comp/math-comp/pull/58#discussion_r76048943
2016-08-17Removing calls of "Context.Named.Declaration.to_tuple" functionMatej Kosik
2016-08-17use a convenient module alias instead of "Context.Rel.Declaration" and ↵Matej Kosik
"Context.Named.Declaration"
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 12:34:32 +0000