aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
AgeCommit message (Collapse)Author
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-02fix debug printEnrico Tassi
2016-02-01compilation on trunk fixedEnrico Tassi
2016-01-31Partially fixing ML compilation on trunk.Pierre-Marie Pédrot
2016-01-12Move bullet initialization to ssreflect.vRobbert Krebbers
2016-01-08fix version number in initialization messageEnrico Tassi
2015-12-04update license banner in .ml filesEnrico Tassi
2015-12-03Removing the only use of globTacticIn.Pierre-Marie Pédrot
2015-12-03fix compilation on trunk (thanks PMP)Enrico Tassi
2015-12-03fix: autogen + abstract variables clashEnrico Tassi
2015-12-03fix: elim/v handles eliminator from Derive Inversion (issue #2)Enrico Tassi
Also: - fix elim trying to saturate too much and not raising the expected exn - fix fill_occ_pattern when occ is {-}, it used to lose the instantiation obtained by matching the term
2015-12-03Add commands to trace the matching algorithmEnrico Tassi
2015-12-03fix: Hint View is not a QueryEnrico Tassi
2015-09-27fix compilation on trunkEnrico Tassi
2015-07-21keeping track of the changes for trunk (import from svn)Cyril Cohen
2015-04-02plugin that compiles with 8.5Enrico Tassi
2015-03-09Initial commitEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:57:54 +0000