aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
AgeCommit message (Collapse)Author
2016-06-16Port build system to trunk (ssrmatching merged in Coq)Enrico Tassi
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-03-27Fixing ML compilation.Pierre-Marie Pédrot
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-22rewrite: matching do not instantiate goal evarsEnrico Tassi
2016-02-03resolve type classes under the correct set of univs (fix #22)Enrico Tassi
2016-02-02Do not hide critical errors with a blind catch all (fix #19)Enrico Tassi
2016-02-02Explicit error message if rewrite fails due to TC inference (fix #21)Enrico Tassi
2016-01-31Partially fixing ML compilation on trunk.Pierre-Marie Pédrot
2016-01-31half-repair compilation on trunkEnrico Tassi
2015-12-04update license banner in .ml filesEnrico 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-07-22blind patch by EnricoCyril Cohen
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-03-02 10:55:23 +0000