aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-29Merge PR #12393: [declare] Miscellaneous nits from my main dev treeGaëtan Gilbert
2020-05-29Merge PR #12421: Fixes for compilation without native dynlinkEmilio Jesus Gallego Arias
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
2020-05-28Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.Hugo Herbelin
2020-05-28Fixing compilation with -natdynlink no.Hugo Herbelin
2020-05-27Merge PR #12389: Small coq_makefile improvement.Enrico Tassi
2020-05-27Adding changelog.Martin Bodin
2020-05-27Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters s...Martin Bodin
2020-05-27Merge PR #12408: Fix output tests for location errors when running in async m...Emilio Jesus Gallego Arias
2020-05-26[declare] Split univs_poly_private in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Factor common universe computation in close proof.Emilio Jesus Gallego Arias
2020-05-26[declare] Split univs_deferred in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Factor out universe computation in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Nit on errors.Emilio Jesus Gallego Arias
2020-05-26[declare] Turn restrict_ucontext hack into an internal parameterEmilio Jesus Gallego Arias
2020-05-26[nit] Remove unused exported error message in obligationsEmilio Jesus Gallego Arias
2020-05-26[declare] Don't expose internal parameter oblsEmilio Jesus Gallego Arias
2020-05-26[declare] Simplify exported type of definition_entryEmilio Jesus Gallego Arias
2020-05-26Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugsGaëtan Gilbert
2020-05-26Merge PR #12388: Fix an uncaught python exception in timingGaëtan Gilbert
2020-05-25dev/tools/make-changelog.sh now asks about fixed bugsJason Gross
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
2020-05-25Merge PR #12403: Fix hyperlinks in changes.rstThéo Zimmermann
2020-05-25Add a changelog.Pierre-Marie Pédrot
2020-05-25Remove the prolog tactic.Pierre-Marie Pédrot
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-21Fix an uncaught python exception in timingJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-22 00:14:59 +0000