aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR #7897: Remove fourier pluginGravatar Enrico Tassi2018-07-18
|\
* \ Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence`Gravatar Enrico Tassi2018-07-18
|\ \
* \ \ Merge PR #8060: Remove useless libobject in proof_usingGravatar Enrico Tassi2018-07-18
|\ \ \
* \ \ \ Merge PR #8055: Fast accumulator check in native compilationGravatar Maxime Dénès2018-07-17
|\ \ \ \
| | | | * Remove fourier pluginGravatar Maxime Dénès2018-07-17
| |_|_|/ |/| | |
* | | | Merge PR #8069: Only check overlay extensions on git-tracked filesGravatar Gaëtan Gilbert2018-07-16
|\ \ \ \
| * | | | Only check overlay extensions on git-tracked filesGravatar Jason Gross2018-07-16
|/ / / /
* | | | Merge PR #8023: Introduce a team of code owners for the CI system.Gravatar Maxime Dénès2018-07-16
|\ \ \ \
* \ \ \ \ Merge PR #8066: [ltac] Remove unused functions.Gravatar Pierre-Marie Pédrot2018-07-16
|\ \ \ \ \
| | | | | * [build] Build Coq and plugins with `-strict-sequence`Gravatar Emilio Jesus Gallego Arias2018-07-14
| |_|_|_|/ |/| | | |
| * | | | [ltac] Remove unused functions / constructors.Gravatar Emilio Jesus Gallego Arias2018-07-14
|/ / / /
* | | | Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of th...Gravatar Théo Zimmermann2018-07-13
|\ \ \ \
| | | | * Remove useless libobject in proof_usingGravatar Maxime Dénès2018-07-13
* | | | | Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib.Gravatar Emilio Jesus Gallego Arias2018-07-13
|\ \ \ \ \
| * | | | | Make -warn-error fail on warnings emitted by coqc on stdlib.Gravatar Maxime Dénès2018-07-13
|/ / / / /
| | | * | Generate type-specific code for is_accu in native compilation of fixpoints.Gravatar Pierre-Marie Pédrot2018-07-13
| | | * | Store the {struct} inductive type in native fixpoint AST.Gravatar Pierre-Marie Pédrot2018-07-13
| | | * | Pass a proper environment to Nativelambda.lambda_of_constr.Gravatar Pierre-Marie Pédrot2018-07-13
| * | | | Fixed typos, wording and grammar errors in the Preamble of the Reference Manu...Gravatar Zeimer2018-07-12
* | | | | Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes`Gravatar Gaëtan Gilbert2018-07-12
|\ \ \ \ \ | |_|_|/ / |/| | | |
* | | | | Merge PR #7907: Tactic deprecation machineryGravatar Pierre-Marie Pédrot2018-07-12
|\ \ \ \ \ | |_|/ / / |/| | | |
* | | | | Merge PR #8051: Clean-up user-overlays folder.Gravatar Emilio Jesus Gallego Arias2018-07-12
|\ \ \ \ \
| * | | | | Clean-up user-overlays folder.Gravatar Théo Zimmermann2018-07-12
| | |_|_|/ | |/| | |
| | | * | [warnings] Disable warning 58 "no cmx file was found in path"Gravatar Emilio Jesus Gallego Arias2018-07-12
| | | * | [warnings] Disable warning 59 [assignment to a non-mutable value] to make fla...Gravatar Emilio Jesus Gallego Arias2018-07-12
| | | * | [ci] Remove warning jobs in favor of default `-warn-error yes`Gravatar Emilio Jesus Gallego Arias2018-07-12
| |_|/ / |/| | |
* | | | Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gravatar Gaëtan Gilbert2018-07-12
|\ \ \ \ | |/ / / |/| | |
| | * | Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
| |/ / |/| |
| * | [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gravatar Emilio Jesus Gallego Arias2018-07-11
|/ /
* | Merge PR #7998: [coqpp] Move to its own directory.Gravatar Pierre-Marie Pédrot2018-07-11
|\ \
* \ \ Merge PR #8035: Fix #8033: Tactic assert-suceeds has a typo in its name in th...Gravatar Théo Zimmermann2018-07-11
|\ \ \
* \ \ \ Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integersGravatar Pierre-Marie Pédrot2018-07-11
|\ \ \ \
* \ \ \ \ Merge PR #8002: make-both-single-timing-files: fix --sort-by=diffGravatar Jason Gross2018-07-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7898: Remove camlp4 remainsGravatar Emilio Jesus Gallego Arias2018-07-11
|\ \ \ \ \ \
| | | | | * | [coqpp] Move to its own directory.Gravatar Emilio Jesus Gallego Arias2018-07-11
| |_|_|_|/ / |/| | | | |
* | | | | | Merge PR #7984: Compile `coqpp` inside the `bin/` folder and make it availabl...Gravatar Emilio Jesus Gallego Arias2018-07-11
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it.Gravatar Emilio Jesus Gallego Arias2018-07-11
|\ \ \ \ \ \ \
| | * | | | | | Compile coqpp inside the bin/ folder and make it available after installation.Gravatar Pierre-Marie Pédrot2018-07-10
| |/ / / / / / |/| | | | | |
* | | | | | | Merge PR #8036: [travis] Remove even more jobs.Gravatar Emilio Jesus Gallego Arias2018-07-10
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #8034: [travis] Try to workaround the repeated APT failures by using...Gravatar Emilio Jesus Gallego Arias2018-07-10
|\ \ \ \ \ \ \ \
| | * | | | | | | [travis] Remove even more jobs.Gravatar Théo Zimmermann2018-07-10
| |/ / / / / / / |/| | | | | | |
| | | | | | * | fixed typo for assert_suceedGravatar charguer2018-07-10
| |_|_|_|_|/ / |/| | | | | |
| * | | | | | [travis] Try to workaround the repeated APT failures by using Jason Gross's s...Gravatar Théo Zimmermann2018-07-10
|/ / / / / /
| * / / / / Remove auto-retry in GitLab CI now that @coqbot is handling it.Gravatar Théo Zimmermann2018-07-10
|/ / / / /
* | | | | Merge PR #7899: My recent improvements to the backport script.Gravatar Maxime Dénès2018-07-10
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7983: Turn a dead branch into an assertion failure in VM reification.Gravatar Maxime Dénès2018-07-10
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #8028: Fix a few typosGravatar Théo Zimmermann2018-07-10
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #8025: Fix rst syntax for `quote ident {ident}`Gravatar Théo Zimmermann2018-07-10
|\ \ \ \ \ \ \ \
| | | | * | | | | Add new options --no-conflict and --no-signature-check to backport script.Gravatar Théo Zimmermann2018-07-10
| |_|_|/ / / / / |/| | | | | | |
| | * | | | | | Fix typo in doc/proof-engine/tactics.rst.Gravatar whitequark2018-07-10