aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2016-03-31Merge pull request #38 from ppedrot/partial-fixEnrico
Fixing ML compilation.
2016-03-27Fixing ML compilation.Pierre-Marie Pédrot
2016-03-15Merge pull request #34 from strub/masterEnrico
all_algebra now exports zmodp
2016-03-15all_algebra now exports zmodpPierre-Yves Strub
2016-03-03Merge pull request #33 from ejgallego/search-print-with-msgEnrico
[search] Use msg_info to notify search results.
2016-03-03[search] Use msg_info to notify search results.Emilio Jesus Gallego Arias
By default, the search command calls `Pp.msg` to print search results. Unfortunately, this bypasses the `log_via_feedback` option and produces not very nice results on feedback-depending IDES like JsCoq. A proper fix would involve merging coq/coq#143 , and the upcoming search cleanup, but this should do the trick for now. I couldn't observe any problem with the usual testing.
2016-03-03fix local opam fileCyril Cohen
2016-03-02fix compilation of ssrmatching in trunkEnrico Tassi
2016-03-02Merge pull request #32 from hivert/patch-1Yves Bertot
Fix the address of the wiki.
2016-03-02Fix the address if the wiki. Florent Hivert
The previous fix wasn't right.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 23:30:58 +0000