aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\
* \ Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Maxime Dénès2017-08-01
|\ \
* \ \ Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.Gravatar Maxime Dénès2017-08-01
|\ \ \
* \ \ \ Merge PR #806: closing bug 5315Gravatar Maxime Dénès2017-08-01
|\ \ \ \
| | | | * Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
* | | | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | * | | closing bug 5315Gravatar Julien Forest2017-07-29
| |/ / / |/| | |
* | | | Merge PR #889: Removing template polymorphism for definitions.Gravatar Maxime Dénès2017-07-28
|\ \ \ \
| | * | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | | * Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Pierre Letouzey2017-07-26
| |_|_|/ |/| | |
* | | | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Gravatar Maxime Dénès2017-07-26
|\ \ \ \ | |_|/ / |/| | |
| | | * Removing default evar-normalization for ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2017-07-26
| |_|/ |/| |
| | * Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
| |/ |/|
* | Merge PR #905: [api] Remove type equalities from API.Gravatar Maxime Dénès2017-07-26
|\ \
* \ \ Merge PR #857: Extraction: various fixes related with bug 4720Gravatar Maxime Dénès2017-07-26
|\ \ \
* \ \ \ Merge PR #859: Extraction TestCompileGravatar Maxime Dénès2017-07-26
|\ \ \ \
| | | * | [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| |_|/ / |/| | |
| | | * Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Gravatar Pierre Letouzey2017-07-25
| |_|/ |/| |
| | * Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
| |/ |/|
* | Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \
* | | [funind] Remove spurious character in comment.Gravatar Emilio Jesus Gallego Arias2017-07-17
* | | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* | | Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
* | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
* | | Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
| | * Extraction TestCompile foo : a new command for extraction + ocamlcGravatar Pierre Letouzey2017-07-05
| |/ |/|
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* | Merge PR#843: closing bug #5618 introduce by PR 828Gravatar Maxime Dénès2017-06-30
|\ \
| * | closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
* | | Merge PR#828: closing bug #4250Gravatar Maxime Dénès2017-06-26
|\| |
* | | Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \ \
| | * | closing bug #4250Gravatar Julien Forest2017-06-23
| |/ / |/| |
* | | Merge PR#807: romega: fix a slowdownGravatar Maxime Dénès2017-06-20
|\ \ \
* \ \ \ Merge PR#803: Clean ssrGravatar Maxime Dénès2017-06-20
|\ \ \ \
| | * | | romega: avoid potential slowdown when changing concl by reified versionGravatar Pierre Letouzey2017-06-16
| * | | | Removing Proof_type from the API.Gravatar Pierre-Marie Pédrot2017-06-16
| * | | | Remove the last use of the low-level Proof_type API in ssr.Gravatar Pierre-Marie Pédrot2017-06-16
| |/ / /
* | | | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* | | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
|/ / /
* | | Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \ \
| | * | plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* | | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \ \
* \ \ \ \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR#673: Two fixes about zify (bugs #5336 and #5439)Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#622: Change the default flag value for Refine.refineGravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \ \
* | | | | | | | Recdef do now a Require Export FunInd (better compat)Gravatar Pierre Letouzey2017-06-14
* | | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* | | | | | | | Makefile.build : cleanup now that micromega.ml isn't generated + sync check o...Gravatar Pierre Letouzey2017-06-14
| | | | | | * | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |_|_|_|_|/ / |/| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 08:20:00 +0000