aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin/v8.5
AgeCommit message (Expand)Author
2018-04-20remove ssr plugin for 8.4 and 8.5Enrico Tassi
2018-03-21Declare prenex implicits for `Some_inj`Anton Trunov
2017-11-14Update v8.5 plugin to fix math-comp/math-comp#61Erik Martin-Dorel
2017-10-30Fix obsolete vernacular syntax for locality.Maxime Dénès
2017-06-09fix compilation on 8.5Enrico Tassi
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-07update copyright bannerAssia Mahboubi
2016-10-24removing the need of bracket to delimit ssrpatternargCyril Cohen
2016-09-27Add a typing colon in the output of the Search ssreflect vernacular.Erik Martin-Dorel
2016-06-16Port build system to trunk (ssrmatching merged in Coq)Enrico Tassi
2016-03-03[search] Use msg_info to notify search results.Emilio Jesus Gallego Arias
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-18type in error messagethery
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-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-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-03fix: autogen + abstract variables clashEnrico Tassi
2015-12-03fix: elim/v handles eliminator from Derive Inversion (issue #2)Enrico Tassi
2015-12-03Add commands to trace the matching algorithmEnrico Tassi
2015-12-03fix: Hint View is not a QueryEnrico Tassi
2015-09-24Fix compilation on 8.5Enrico Tassi
2015-08-24Compare pattern heads (constants) up to "univs"Enrico Tassi
2015-07-17Updating files + reorganizing everythingCyril 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-05 12:19:50 +0000