aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
AgeCommit message (Collapse)Author
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-21Merge pull request #108 from ejgallego/pp_new_fixMaxime Dénès
Use pp_with as msg_with is being removed upstream.
2017-03-13Reflection lemmas for `seq.uniq`Pierre-Yves Strub
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.
2016-12-20correct a typo in the documentationYves Bertot
2016-12-19fix compilation on 8.5Enrico Tassi
2016-12-06backport Coq PR#387 on ssrmatching for Coq v8.5Enrico 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-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-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-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-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-26fix compilation wrt. commit 69388fc in Coq trunkMatej Kosik
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-14 00:56:32 +0000