aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-10-12Merge pull request #76 from matej-kosik/masterEnrico
changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's "pr_o.cmo" plugin
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-28Merge pull request #73 from erikmd/patch-searchEnrico
Add a typing colon in the output of the Search ssreflect vernacular
2016-09-27Add a typing colon in the output of the Search ssreflect vernacular.Erik Martin-Dorel
2016-09-26Merge pull request #72 from ppedrot/partial-fixEnrico
Fix ML compilation after Ltac refactoring.
2016-09-24Fix ML compilation after Ltac refactoring.Pierre-Marie Pédrot
2016-09-23Merge pull request #71 from matej-kosik/masterEnrico
FIX: compilation wrt. commit 9c35248 on Coq trunk branch.
2016-09-23FIX: compilation wrt. commit 9c35248 on Coq trunk branch.Matej Kosik
2016-09-22Merge pull request #70 from matej-kosik/masterEnrico
fix compilation wrt. commit 699b70c in Coq trunk
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-19Merge pull request #67 from ppedrot/partial-fixEnrico
Fix compilation after change in CErrors API.
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-28Merge pull request #60 from matej-kosik/masterEnrico
fix compilation wrt. commit 69388fc in Coq trunk
2016-08-26fix compilation wrt. commit 69388fc in Coq trunkMatej Kosik
2016-08-25Merge pull request #59 from matej-kosik/masterEnrico
FIX: adding missing version of the ssreflect plugin that compiles with Coq 8.6
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-24Merge pull request #58 from matej-kosik/masterEnrico
Removing calls of "Context.Named.Declaration.{of,to}_tuple" functions
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"
2016-08-16fix compilation on trunk (thanks Matej)Enrico Tassi
2016-07-03Fix compilation after Errors and Closure were renamed.Maxime Dénès
2016-07-01Fix compilation after renaming of reduction functions and flags in Coq.Maxime Dénès
2016-06-17fix parsing (coq trunk goal selector/ltac:)Enrico Tassi
2016-06-17this test is now in Coq, removing it.Enrico Tassi
2016-06-16Port build system to trunk (ssrmatching merged in Coq)Enrico Tassi
2016-06-03Merge pull request #49 from matej-kosik/masterEnrico
fixing compilation (with Coq trunk & Coq v8.5)
2016-06-03fixing compilation (with Coq trunk & Coq v8.5)Matej Kosik
2016-06-01Merge pull request #48 from ejgallego/pp_cleanup_fixEnrico
Compatibility with latest Coq trunk.
2016-05-31Compatibility with latest Coq trunk.Emilio Jesus Gallego Arias
2016-05-18Merge pull request #46 from ppedrot/partial-fixEnrico
Fix compilation after the change of API in Tactics.
2016-05-18Fix compilation after the change of API in Tactics.Pierre-Marie Pédrot
2016-05-16Merge pull request #44 from ppedrot/partial-fixEnrico
Fix compilation after the renaming of Lexer into CLexer.
2016-05-16Fix compilation after the renaming of Lexer into CLexer.Pierre-Marie Pédrot
2016-05-12Merge pull request #43 from hivert/fixdocGeorges Gonthier
Fixes the doc of mxrepresentation.v
2016-05-12Fixes doc of mxrepresentation.vFlorent Hivert
2016-05-09Merge pull request #42 from ppedrot/partial-fixEnrico
Fix compilation after the merge of the dynamic tactic value branch.
2016-05-09Fix compilation after the merge of the dynamic tactic value branch.Pierre-Marie Pédrot
2016-05-04Merge pull request #40 from ppedrot/partial-fixEnrico
Fixing compilation after the merge of ML-tactic-notation branch.
2016-05-02Fixing compilation after the merge of ML-tactic-notation branch.Pierre-Marie Pédrot
2016-04-15Merge pull request #39 from ppedrot/partial-fixEnrico
Fixing compilation after the merge of PR trunk-function_scope.
2016-04-08Fixing compilation after the merge of PR trunk-function_scope.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:45:02 +0000