aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
AgeCommit message (Collapse)Author
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-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
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-12changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's ↵Matej Kosik
"pr_o.cmo" plugin
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-16Fix compilation after change in CErrors API.Pierre-Marie Pédrot
2016-08-26fix compilation wrt. commit 69388fc in Coq trunkMatej Kosik
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
2016-05-16Fix compilation after the renaming of Lexer into CLexer.Pierre-Marie Pédrot
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-03-27Fixing ML compilation.Pierre-Marie Pédrot
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-02-22Guard "catch all" exception handler using Errors.noncriticalEnrico Tassi
2016-02-18typo in error messagethery
2016-02-15Removing compatibility layers.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:35:26 +0000