coq/doc/changelog/08-tools, branch master The formal proof system Clarify changelog categories. 2020-12-11T09:02:30+00:00 Théo Zimmermann 2020-12-11T09:02:27+00:00 1605ae821f151f1e4b4edab9a0dded02cb91eebf For readers of the changelog: title "Tools" become "Command-line tools". For developers: changelog categories 07 and 08 are disambiguated. 
For readers of the changelog: title "Tools" become "Command-line tools".
For developers: changelog categories 07 and 08 are disambiguated.
[changelog] update markup 2020-12-03T15:03:37+00:00 Enrico Tassi 2020-11-30T09:03:47+00:00 c8fc6b8f0d357b01f919b8346f45d0bd020f4fe2 






Changes for Coq 8.13
2020-12-03T15:03:37+00:00

Matthieu Sozeau

2020-11-30T16:12:37+00:00

3c4d2c9e3b7100a0012ad06b33b46fe7dca6cd29












Changelog for 8.12.1.
2020-11-05T15:47:36+00:00

Théo Zimmermann

2020-11-05T15:47:36+00:00

a6b5a5a66b59750148ead34148cfefd1702a64e0












Make print-pretty-timed robust against non-output-sync logs
2020-09-21T16:42:14+00:00

Jason Gross

2020-09-21T16:38:25+00:00

fef5b75e72e1dc2889875616f56332a00dc50534

Also pass `--output-sync` on the CI, as suggested in
https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect
against this failure mode.

Fixes #13062





Also pass `--output-sync` on the CI, as suggested in
https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect
against this failure mode.

Fixes #13062







[coqchk] Look inside inner modules as well
2020-08-19T19:09:42+00:00

Jason Gross

2020-08-19T18:41:19+00:00

cfc54842c2a71b7cdb8c59e3ce9fe4a13cedb5ae

Fixes #12845 (coqchk reports names from inner modules of opaque modules
as axioms)

I don't fully understand the code here, so I can't speak as to its
correctness, but it should be simple enough that reviewers can
understand what it's doing and whether or not it's correct.

This is useful for me in making progress towards
https://github.com/mit-plv/fiat-crypto/issues/736





Fixes #12845 (coqchk reports names from inner modules of opaque modules
as axioms)

I don't fully understand the code here, so I can't speak as to its
correctness, but it should be simple enough that reviewers can
understand what it's doing and whether or not it's correct.

This is useful for me in making progress towards
https://github.com/mit-plv/fiat-crypto/issues/736







coqdoc: Fix the “details” environment
2020-07-29T15:48:22+00:00

Thomas Letan

2020-07-29T12:53:19+00:00

ce233d5b4a6f8d506c37a2a492679a66f9618a94

The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.





The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.







Adding change log for #12754.
2020-07-24T20:40:40+00:00

Hugo Herbelin

2020-07-24T20:40:40+00:00

23303e6d2129e4e63252643fc84f42ac8dcec48c












Remove deprecated (in 8.8 #6277) coqchk -I
2020-07-01T10:12:06+00:00

Gaëtan Gilbert

2020-06-30T19:40:22+00:00

828b84e81625c80403860d58756bddd760e6ee34












Merge PR #12396: Release notes 8.12
2020-06-01T14:37:55+00:00

Emilio Jesus Gallego Arias

2020-06-01T14:37:55+00:00

a1fa186fc8314e395a0813bb23c2c73d738b7572

Reviewed-by: ejgallego
Ack-by: jfehrle





Reviewed-by: ejgallego
Ack-by: jfehrle