aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2017-08-01adding a comment to explain the changeJulien Forest
2017-08-01solving b1859Julien Forest
2017-07-31Improve errors for cumulativity when monomorphicAmin Timany
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-31Correcting [build_discriminator] to make the test-suite passamblaf
2017-07-29closing bug 5315Julien Forest
2017-07-28Merge PR #889: Removing template polymorphism for definitions.Maxime Dénès
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Extraction: reduce primitive projections in types (fix bug 4709)Pierre Letouzey
2017-07-26Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Maxime Dénès
2017-07-26Removing default evar-normalization for ARGUMENT EXTEND.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-26Merge PR #905: [api] Remove type equalities from API.Maxime Dénès
2017-07-26Merge PR #857: Extraction: various fixes related with bug 4720Maxime Dénès
2017-07-26Merge PR #859: Extraction TestCompileMaxime Dénès
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-25Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Pierre Letouzey
2017-07-20Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Pierre Letouzey
2017-07-19Merge PR #770: [proof] Move bullets to their own module.Maxime Dénès
2017-07-17[funind] Remove spurious character in comment.Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
2017-07-13Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Pierre-Marie Pédrot
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-05Extraction TestCompile foo : a new command for extraction + ocamlcPierre Letouzey
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-30Merge PR#843: closing bug #5618 introduce by PR 828Maxime Dénès
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-27Preparing to hints supporting discharge.Hugo Herbelin
2017-06-26Merge PR#828: closing bug #4250Maxime Dénès
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-23closing bug #4250Julien Forest
2017-06-20Merge PR#807: romega: fix a slowdownMaxime Dénès
2017-06-20Merge PR#803: Clean ssrMaxime Dénès
2017-06-16romega: avoid potential slowdown when changing concl by reified versionPierre Letouzey
2017-06-16Removing Proof_type from the API.Pierre-Marie Pédrot
2017-06-16Remove the last use of the low-level Proof_type API in ssr.Pierre-Marie Pédrot
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#763: [proof] Deprecate redundant wrappers.Maxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14Merge PR#673: Two fixes about zify (bugs #5336 and #5439)Maxime Dénès
2017-06-14Merge PR#622: Change the default flag value for Refine.refineMaxime Dénès
2017-06-14Recdef do now a Require Export FunInd (better compat)Pierre Letouzey
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-14Makefile.build : cleanup now that micromega.ml isn't generated + sync check o...Pierre Letouzey
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 06:41:39 +0000