aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin
AgeCommit message (Expand)Author
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 "pr_o.c...Matej Kosik
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
2016-08-24Possible code compaction motivated by Enrico's remark: https://github.com/ma...Matej Kosik
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 "Conte...Matej Kosik
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
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
2016-02-02Explicit error message if rewrite fails due to TC inference (fix #21)Enrico Tassi
2016-02-01compilation on trunk fixedEnrico Tassi
2016-01-31Partially fixing ML compilation on trunk.Pierre-Marie Pédrot
2016-01-31half-repair compilation on trunkEnrico Tassi
2016-01-12Move bullet initialization to ssreflect.vRobbert Krebbers
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:28:22 +0000