aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-26Fix #12280: do not use xindy to avoid build failures on some machines.Théo Zimmermann
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
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 ↵Pierre-Marie Pédrot
modules as axioms) Reviewed-by: herbelin Reviewed-by: ppedrot
2020-05-22[coqchk] Improve previous heuristic.Pierre Roux
Instead of considering all constants without body in the environment, consider only the ones appearing in the body of the opacified constant.
2020-05-22[coqchk] Add testPierre Roux
2020-05-22[coqchk] Fix #5030Pierre Roux
When encountering ```Coq Module M : T. ... Lemma c :... ... Qed. ... End M. ``` every field `c` without body in `T` but with a body in `M` is registered as opacified in a table along with all constants `opacified(c)` without body in the environment at this point (i.e., all axioms potentially used by c). Then, when printing axioms, if `c` appears in the final environment it is replaced by `opacified(c)` in the resulting list of axioms.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 02:59:15 +0000