aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin
AgeCommit message (Collapse)Author
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
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-09-24Fix compilation on 8.5Enrico Tassi
2015-08-24Compare pattern heads (constants) up to "univs"Enrico Tassi
So that Universe Polymorphic constants are compared "correctly", i.e. not discriminated by the pattern filtering phase (verbatim head comparison) but eventually by unification.
2015-07-30fix trunk compilationEnrico Tassi
2015-07-22blind patch by EnricoCyril Cohen
2015-07-21keeping track of the changes for trunk (import from svn)Cyril Cohen
2015-07-18update to preserve backward compatibility with v8.4Cyril Cohen
2015-07-17Updating files + reorganizing everythingCyril Cohen
2015-04-09support for camlp4Enrico Tassi
2015-04-09Forward compatibility with "From X Require Y."Enrico Tassi
2015-04-02support both coq.8.5beta1 and coq.8.5.devEnrico Tassi
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-28 22:11:32 +0000