| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |||
| 2016-05-12 | Fixes doc of mxrepresentation.v | Florent Hivert | |
| 2016-05-09 | Fix compilation after the merge of the dynamic tactic value branch. | Pierre-Marie Pédrot | |
| 2016-05-02 | Fixing compilation after the merge of ML-tactic-notation branch. | Pierre-Marie Pédrot | |
| 2016-04-08 | Fixing compilation after the merge of PR trunk-function_scope. | Pierre-Marie Pédrot | |
| 2016-03-27 | Fixing ML compilation. | Pierre-Marie Pédrot | |
| 2016-03-15 | Merge pull request #34 from strub/master | Enrico | |
| all_algebra now exports zmodp | |||
| 2016-03-15 | all_algebra now exports zmodp | Pierre-Yves Strub | |
| 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-03 | fix local opam file | Cyril Cohen | |
| 2016-03-02 | fix compilation of ssrmatching in trunk | Enrico Tassi | |
| 2016-02-25 | fix compilation | Enrico Tassi | |
| 2016-02-25 | ssrpattern: compose nicely with Tactic Notation | Enrico Tassi | |
| 2016-02-22 | Guard "catch all" exception handler using Errors.noncritical | Enrico Tassi | |
| 2016-02-22 | rewrite: matching do not instantiate goal evars | Enrico Tassi | |
| 2016-02-22 | PF5: more predictable rewrite line (needed by rewrite using 8.5 refiner) | Enrico Tassi | |
| 2016-02-18 | typo in error message | thery | |
| 2016-02-18 | type in error message | thery | |
| 2016-02-15 | Removing compatibility layers. | Pierre-Marie Pédrot | |
| 2016-02-15 | Fixing ML compilation with trunk. | Pierre-Marie Pédrot | |
| 2016-02-09 | [div] Move dvdn_fact from prime to div. | Emilio Jesus Gallego Arias | |
| 2016-02-06 | typo in int divn1 -> divz1 | thery | |
| 2016-02-03 | Register flag "SsrHave NoTCResolution" in the Summary (fix #6) | Enrico Tassi | |
| 2016-02-03 | resolve type classes under the correct set of univs (fix #22) | Enrico Tassi | |
| 2016-02-02 | fix compilation on 8.4 | Enrico Tassi | |
| 2016-02-02 | Do not hide critical errors with a blind catch all (fix #19) | Enrico Tassi | |
| 2016-02-02 | fix debug print | Enrico Tassi | |
| 2016-02-02 | Explicit error message if rewrite fails due to TC inference (fix #21) | Enrico Tassi | |
| 2016-02-01 | compilation on trunk fixed | Enrico Tassi | |
| 2016-01-31 | Partially fixing ML compilation on trunk. | Pierre-Marie Pédrot | |
| 2016-01-31 | half-repair compilation on trunk | Enrico Tassi | |
| 2016-01-22 | generalizing odd_opp | Cyril Cohen | |
| 2016-01-21 | build script is now cygwin friendly | Enrico Tassi | |
| symlinks are not first class citizens on windows | |||
| 2016-01-12 | Move bullet initialization to ssreflect.v | Robbert Krebbers | |
| 2016-01-08 | fix version number in initialization message | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |