aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
AgeCommit message (Collapse)Author
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-09[div] Move dvdn_fact from prime to div.Emilio Jesus Gallego Arias
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-22generalizing odd_oppCyril Cohen
2016-01-21build script is now cygwin friendlyEnrico Tassi
symlinks are not first class citizens on windows
2016-01-12Move bullet initialization to ssreflect.vRobbert Krebbers
2016-01-08fix version number in initialization messageEnrico Tassi
2015-12-26removing mathcomp dir when removing ssreflectCyril Cohen
2015-12-12switch ":" to "-"Cyril Cohen
2015-12-04update license banner in .ml filesEnrico Tassi
2015-12-04Merge branch 'master' of https://github.com/math-comp/math-compGeorges Gonthier
2015-12-04Remove redundant structures for finite powersGeorges Gonthier
2015-12-04fix coq-mathcomp-ssreflect opam package descriptionEnrico 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-11-30Typos in comments.Assia Mahboubi
2015-11-20Typo.Assia Mahboubi
2015-11-20TyposAssia Mahboubi
2015-11-10fix INSTALL symlinksEnrico Tassi
2015-11-05merge basic/ into ssreflect/Enrico Tassi
2015-10-26Added support for highlighting 'isn't' in PG.Assia Mahboubi
2015-10-26Added suport for highlighting gen(erally) have in PG.Assia Mahboubi
2015-10-26Small updates in the documentation of the customization of PG.Assia Mahboubi
2015-10-26Restaured the config files (including doc) for PG in the ssreflect package.Assia Mahboubi
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-29fix MakefilesEnrico Tassi
2015-07-28update copyright bannerEnrico Tassi
2015-07-28factor common Makefile stuffEnrico Tassi
2015-07-22blind patch by EnricoCyril Cohen
2015-07-22remove duplicate fieldsCyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 17:34:38 +0000