aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin
AgeCommit message (Collapse)Author
2017-04-07[camplX] Remove camlp4 support.Emilio Jesus Gallego Arias
Adapting to Coq upstream.
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-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-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-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-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
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 01:37:15 +0000