aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Collapse)Author
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-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
2016-11-08fix compilation on 8.6 and trunkEnrico Tassi
2016-11-07update copyright bannerAssia Mahboubi
2016-10-24removing the need of bracket to delimit ssrpatternargCyril Cohen
2016-10-24wip shorter proof dec factor theoremsCyril Cohen
2016-10-24better ltngtPCyril Cohen
2016-10-13Make: avoid >> Make, pass args to coq_makefile instead (#77)Enrico Tassi
2016-10-13Merge pull request #65 from gares/masterCyril Cohen
abstract_context utility lemma
2016-10-13Merge pull request #66 from thery/masterCyril Cohen
Adding theorems in binomial
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-27Add a typing colon in the output of the Search ssreflect vernacular.Erik Martin-Dorel
2016-09-24Fix ML compilation after Ltac refactoring.Pierre-Marie Pédrot
2016-09-23FIX: compilation wrt. commit 9c35248 on Coq trunk branch.Matej Kosik
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-21 12:01:37 +0000