aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Collapse)Author
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-03fixing compilation (with Coq trunk & Coq v8.5)Matej Kosik
2016-05-31Compatibility with latest Coq trunk.Emilio Jesus Gallego Arias
2016-05-18Fix compilation after the change of API in Tactics.Pierre-Marie Pédrot
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-09Fix compilation after the merge of the dynamic tactic value branch.Pierre-Marie Pédrot
2016-05-02Fixing compilation after the merge of ML-tactic-notation branch.Pierre-Marie Pédrot
2016-04-08Fixing compilation after the merge of PR trunk-function_scope.Pierre-Marie Pédrot
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-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-02-25fix compilationEnrico Tassi
2016-02-25ssrpattern: compose nicely with Tactic NotationEnrico Tassi
2016-02-22Guard "catch all" exception handler using Errors.noncriticalEnrico Tassi
2016-02-22rewrite: matching do not instantiate goal evarsEnrico Tassi
2016-02-22PF5: more predictable rewrite line (needed by rewrite using 8.5 refiner)Enrico Tassi
2016-02-18typo in error messagethery
2016-02-18type in error messagethery
2016-02-15Removing compatibility layers.Pierre-Marie Pédrot
2016-02-15Fixing 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-06typo in int divn1 -> divz1thery
2016-02-03Register flag "SsrHave NoTCResolution" in the Summary (fix #6)Enrico Tassi
2016-02-03resolve type classes under the correct set of univs (fix #22)Enrico Tassi
2016-02-02fix compilation on 8.4Enrico Tassi
2016-02-02Do not hide critical errors with a blind catch all (fix #19)Enrico Tassi
2016-02-02fix debug printEnrico Tassi
2016-02-02Explicit error message if rewrite fails due to TC inference (fix #21)Enrico Tassi
2016-02-01compilation on trunk fixedEnrico Tassi
2016-01-31Partially fixing ML compilation on trunk.Pierre-Marie Pédrot
2016-01-31half-repair compilation on trunkEnrico Tassi
2016-01-22generalizing odd_oppCyril Cohen
2016-01-21build script is now cygwin friendlyEnrico Tassi
symlinks are not first class citizens on windows
2016-01-12Move bullet initialization to ssreflect.vRobbert Krebbers
2016-01-08fix version number in initialization messageEnrico Tassi
2015-12-26removing mathcomp dir when removing ssreflectCyril Cohen
2015-12-14fix compilationEnrico Tassi
2015-12-13fixCyril Cohen
2015-12-12removing trailing whitespaces in opam fileCyril Cohen
2015-12-12changing dependencyCyril Cohen
2015-12-12switch ":" to "-"Cyril Cohen
2015-12-12fixing requires in stripped odd orderCyril Cohen
2015-12-12Revert "HACK: work around regression in 8.5"Enrico Tassi
This reverts commit 006565bdb5b473afff5f834e4b20320bb0a419fd. since Coq commit c6b75e1b693ab8c7af2efd1b93f04eab248e584c make this unnecessary
2015-12-10HACK: work around regression in 8.5Enrico Tassi
This shall be reverted, it is there only to make ssr compile on jenkins and help the release of Coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 01:27:08 +0000