aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-05[sphinx] Remove most pylint warningsClément Pit-Claudel
2020-06-02Merge PR #12412: Reduce options passed to workersEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-06-02Merge PR #11974: Require in Section: warning is now about fragility not ↵Emilio Jesus Gallego Arias
deprecation. Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-06-01Merge PR #12396: Release notes 8.12Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: jfehrle
2020-06-01Merge PR #12422: Fixes #12418: an assert false in inference of return clauseEmilio Jesus Gallego Arias
Reviewed-by: gares
2020-06-01Merge PR #12431: [ci] Split fiat-crypto into non-OCaml and OCamlGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-31[ci] Split fiat-crypto into non-OCaml and OCamlJason Gross
Note that this should reduce the overall build time of fiat-crypto related targets by about 10--20 minutes, as I've removed the heaviest jobs (about 25--30 minutes in serial) from the OCaml target. I'd like to keep the OCaml target around just to make sure that Coq doesn't introduce a change to extraction that breaks compilation of extracted OCaml code. See https://github.com/ocaml/ocaml/issues/7826 for the issue tracking performance of compiling the extracted OCaml code (and perhaps there should be another issue opened on the OCaml bug tracker about flambda on the fiat-crypto extracted files?) Alternative to #12405 Closes #12405 Fixes #12400
2020-05-29Merge PR #12393: [declare] Miscellaneous nits from my main dev treeGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-29Change log for #12422.Hugo Herbelin
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
This is a quick fix to avoid the anomaly, with a fallback on before b1b8243b7fc.
2020-05-29Merge PR #12421: Fixes for compilation without native dynlinkEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
Reviewed-by: Zimmi48
2020-05-28Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.Hugo Herbelin
2020-05-28Fixing compilation with -natdynlink no.Hugo Herbelin
This complements #11407 about storing digests of modules.
2020-05-27Merge PR #12389: Small coq_makefile improvement.Enrico Tassi
Reviewed-by: gares
2020-05-27Adding changelog.Martin Bodin
2020-05-27Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters ↵Martin Bodin
section.
2020-05-27Add more changelog entries which have been backported to v8.12.Théo Zimmermann
2020-05-27[changelog/8.12] Wording improvements.Théo Zimmermann
2020-05-27[changelog/8.12] Use sections and provide a local TOC.Théo Zimmermann
2020-05-27[changelog/8.12] Split misc entries out in more relevant sections.Théo Zimmermann
2020-05-27Changelog entries for the 8.12 changes to the reference manual.Théo Zimmermann
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-27Fix changelog for #11986.Théo Zimmermann
2020-05-27Merge PR #12408: Fix output tests for location errors when running in async ↵Emilio Jesus Gallego Arias
mode. Reviewed-by: JasonGross Reviewed-by: ejgallego
2020-05-26[declare] Split univs_poly_private in close_proofEmilio Jesus Gallego Arias
A step towards enforcing some more static invariants.
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
A step towards enforcing some more static invariants.
2020-05-26[declare] Factor out universe computation in close_proofEmilio Jesus Gallego Arias
A step towards enforcing some more static invariants.
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
This is not needed outside of `Declare` now.
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
This reduces the amount of exported internals, in particular w.r.t. proof delaying and side effects which we will need in future refactorings. Actually turning the type from `Evd.side_effects proof_entry` to `unit proof_entry` is left for the next commits.
2020-05-26Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugsGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-26Merge PR #12388: Fix an uncaught python exception in timingGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-26Fix usage of -rifrom, -refrom.Théo Zimmermann
2020-05-26Fix worker handling of command-line options that are already included in ↵Théo Zimmermann
initial state.
2020-05-26Remove command-line options that do not exist anymore.Théo Zimmermann
2020-05-25dev/tools/make-changelog.sh now asks about fixed bugsJason Gross
Fixes #12386
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
In this mode, an additional error was emitted, which made the test fail: Error: There are pending proofs: Unnamed_thm.
2020-05-25Merge PR #12403: Fix hyperlinks in changes.rstThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-25Add a changelog.Pierre-Marie Pédrot
2020-05-25Remove the prolog tactic.Pierre-Marie Pédrot
It was deprecated in 8.12 and not used in the wild.
2020-05-24Fix hyperlinks in changes.rstMatthew Dempsky
2020-05-24Merge PR #12392: [backport-pr] Select correct remote of the master branch.Jason Gross
Reviewed-by: JasonGross
2020-05-24Merge PR #12379: Omit voluminous Latex warningsThéo Zimmermann
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:22:48 +0000