aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
2020-05-25Merge PR #12403: Fix hyperlinks in changes.rstThéo Zimmermann
2020-05-24Fix hyperlinks in changes.rstMatthew Dempsky
2020-05-24Merge PR #12392: [backport-pr] Select correct remote of the master branch.Jason Gross
2020-05-24Merge PR #12379: Omit voluminous Latex warningsThéo Zimmermann
2020-05-23[dev/tools] Fix #12314: do not die silently if branch has no remote.Théo Zimmermann
2020-05-22[backport-pr] Select correct remote of the master branch.Théo Zimmermann
2020-05-22Merge PR #12076: [coqchk] Fix #5030 (coqchk reports names from opaque modules...Pierre-Marie Pédrot
2020-05-22[coqchk] Improve previous heuristic.Pierre Roux
2020-05-22[coqchk] Add testPierre Roux
2020-05-22[coqchk] Fix #5030Pierre Roux
2020-05-22[coqchk] Change list to setPierre Roux
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...Pierre-Marie Pédrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-21Merge PR #12371: [obligations] Minor refactoringGaëtan Gilbert
2020-05-21Merge PR #12368: Print a newline at the end of timing tablesGaëtan Gilbert
2020-05-21Merge PR #12364: [ci] [docker] Bump ocamlformat and duneGaëtan Gilbert
2020-05-21Merge PR #12358: [topfmt] Set formatter + flush fixGaëtan Gilbert
2020-05-21Merge PR #12316: Use pagination in fetching the number of reviewsGaëtan Gilbert
2020-05-20Print a newline at the end of timing tablesJason Gross
2020-05-20[merge-pr] Use a simpler method to get all pagesJason Gross
2020-05-20[merge-pr.sh] Follow next links insteadJason Gross
2020-05-20Use pagination in fetching the number of reviewsJason Gross
2020-05-20Omit volumnious Latex messagesJim Fehrle
2020-05-20Merge PR #12377: Adapt the documentation to the move from Gitter to Zulip.Clément Pit-Claudel
2020-05-20Adapt the documentation to the move from Gitter to Zulip.Théo Zimmermann
2020-05-20Merge PR #12359: [ci] Add mit-plv/engine-benchGaëtan Gilbert
2020-05-20[obligations] [nit] Refactor obligation printing.Emilio Jesus Gallego Arias
2020-05-20[obligations] `declare_obligation` now takes an `UState.t`Emilio Jesus Gallego Arias
2020-05-20[declare] [nit] Use proper type alias for in ProgramDecl interfaceEmilio Jesus Gallego Arias
2020-05-20[nit] Remove `Declare.Obls.err_not_transp`Emilio Jesus Gallego Arias
2020-05-20Merge PR #12350: [test-suite] Ensure copies of files are writableGaëtan Gilbert
2020-05-20Merge PR #12356: [declare] Remove unused parameters in prepare_obligationGaëtan Gilbert
2020-05-20Merge PR #12354: [universes] [api] Provide UState.from_envGaëtan Gilbert
2020-05-20Merge PR #12342: Direct URL for triggering a pipeline with SKIP_DOCKER=false.Gaëtan Gilbert
2020-05-20Bump nixpkgs to get ocamlformat 0.14.2.Théo Zimmermann
2020-05-20Merge PR #12362: Use dev version for opam git pinning in .gitlab-ci.yml.Emilio Jesus Gallego Arias
2020-05-19[ci] Add mit-plv/engine-benchJason Gross
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
2020-05-19[ci] [docker] Bump ocamlformat and duneEmilio Jesus Gallego Arias
2020-05-19Use dev version for opam git pinning in .gitlab-ci.yml.Théo Zimmermann
2020-05-19Merge PR #12224: Support :gdef:`text<term>` syntax (adding "<term>")Clément Pit-Claudel
2020-05-19[declare] Remove unused parameters in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[declare] Minor tweaks in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[declare] Remove dead code in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[universes] [api] Provide UState.from_envEmilio Jesus Gallego Arias
2020-05-19Merge PR #12353: Update release-process.mdEmilio Jesus Gallego Arias
2020-05-19Merge PR #12301: [declare] Grand unification of the proof save path.Gaëtan Gilbert
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Use the new gdef alt-text feature in the refman.Théo Zimmermann