aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* 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
| |_|_|_|_|/ |/| | | | |
| | | | | * Deprecate options that were introduced for compatibility with 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | | | * Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| |_|_|_|/ |/| | | |
| * | | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| * | | | Explicit the unsafe flag of all calls to Refine.refine.Gravatar Pierre-Marie Pédrot2017-06-13
* | | | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
|/ / / /
* | | | Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ge...Gravatar Matej Košík2017-06-12
* | | | Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\ \ \ \
* \ \ \ \ Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\ \ \ \ \
| | | * | | zify: force reduction of (Z.max 0 0) and similar (fix #5439)Gravatar Pierre Letouzey2017-06-12
| | | * | | zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)Gravatar Pierre Letouzey2017-06-12
| |_|/ / / |/| | | |
| | | | * [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
| |_|_|/ |/| | |
* | | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| * | | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
| | | * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
| |_|/ |/| |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \ | |/ / |/| |
* | | Put "ssreflect" behind "API".Gravatar Matej Košík2017-06-07
* | | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* | | Merge the ssr plugin.Gravatar Maxime Dénès2017-06-06
* | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* | | Merge PR#600: Some factorizations of ltac interpretation functions between ss...Gravatar Maxime Dénès2017-06-06
|\ \ \
* \ \ \ Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \ \ \
* \ \ \ \ Merge PR#722: [printing] Remove duplicated printing function.Gravatar Maxime Dénès2017-06-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Gravatar Maxime Dénès2017-06-05
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#526: solving implicit resolution in FunctionGravatar Maxime Dénès2017-06-04
|\ \ \ \ \ \ \
| | | | * | | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | * | | | Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
| |_|_|/ / / / |/| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 11:20:40 +0000