aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Collapse)Author
2017-10-23Merge pull request #145 from CohenCyril/new-packagerCyril Cohen
New packager
2017-10-20Merge pull request #140 from RalfJung/makeEnrico
fix building with make flags
2017-10-19fixed homepageCyril Cohen
2017-10-19fix coq versionCyril Cohen
2017-10-12fix Coq version detection on Windows, and in case there are errorsRalf Jung
2017-10-10fix building with make flagsRalf Jung
Fixes #139
2017-09-13update the opam description for use in coq.8.7Yves Bertot
2017-09-07Merge pull request #106 from akr/remove-subfilter-docCyril Cohen
remove documentation for subfilter.
2017-08-13Fix typo in fingroup documentationPatrick Massot
2017-07-31Fix build of ssreflect/ only on 8.6Enrico Tassi
2017-07-13trunk -> masterEnrico
2017-06-14No .ml4 file in the standard MakeEnrico
it is to the caller of coq_makefile to eventually add .ml4 files
2017-06-14Fix compilation of ssreflect/ submoduleMatej Košík
2017-06-09fix compilation on 8.5Enrico Tassi
2017-06-09fix compilation on 8.6Enrico Tassi
2017-06-07Change failing test.Maxime Dénès
2017-06-07For trunk, use merged ssr plugin.Maxime Dénès
2017-06-06Fix plugin after Sigma removal.Maxime Dénès
2017-06-06Merge pull request #127 from herbelin/trunk+interp_closed_glob_constrMaxime Dénès
Binding glob_constr to interp_glob_closure so as to factorize low-level code.
2017-05-31Adapting to PR #590 (a more explicit algebraic type for evars of kind ↵Hugo Herbelin
MatchingVar).
2017-05-31Binding glob_constr to interp_glob_closure so as to factorize low-level code.Hugo Herbelin
2017-05-25[coqlib] Update to explicitly build terms from references.Emilio Jesus Gallego Arias
See coq/coq#678
2017-05-25Merge pull request #125 from ejgallego/options+remove_non_syncMaxime Dénès
[options] Sync with upstream API changes.
2017-05-23[options] Sync with upstream API changes.Emilio Jesus Gallego Arias
2017-04-19[ast] Adapt to Coq's #402 new generic AST node.Emilio Jesus Gallego Arias
2017-04-17Coq PR #565: G_vernac.subgoal_command is replaced by query_commandGaetan Gilbert
2017-04-12Merge pull request #119 from maximedenes/econstrMaxime Dénès
Econstr support
2017-04-07[camplX] Remove camlp4 support.Emilio Jesus Gallego Arias
Adapting to Coq upstream.
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-12 05:35:54 +0000