~jgross-h/coq/+git/coq:v8.8

Branch merges

Related source package recipes

2 recipes using this branch. (?)

Create packaging recipe

Related snap packages

Related charm recipes

9632df5... by Jason Gross on 2022-06-23

Merge PR #16238: [v8.8] Backport #15271: Delay removing native_compute .ml files until exit

d71709d... by =?utf-8?q?Ga=C3=ABtan_Gilbert?= <email address hidden> on 2021-11-30

Delay removing native_compute .ml files until exit

Fix #15263 (assuming it was correctly diagnosed)

Co-authored-by: Jason Gross <email address hidden>

0ed45a5... by =?utf-8?q?Th=C3=A9o_Zimmermann?= <email address hidden> on 2018-09-25

Set Coq version to 8.8.2.

d1dcdca... by =?utf-8?q?Th=C3=A9o_Zimmermann?= <email address hidden> on 2018-09-25

Backport PR #8535: Fixing #8532: regression in Print Assumptions within a functor.

1904d16... by Hugo Herbelin <email address hidden> on 2018-09-23

Fixing #8532 (regression in Print Assumptions within a functor).

The regression was introduced in 1522b989 (PR #7193) which itself was
fixing bug #7192. (Note another regression of the same commit which is
fixed in #8416.)

(cherry picked from commit 1ac3418389789e7288c5fb3576f787b7c2544342)

4e5c111... by =?utf-8?q?Th=C3=A9o_Zimmermann?= <email address hidden> on 2018-09-25

Backport PR #8549: Fix issues introduced by the PDF manual merge

d945edd... by =?utf-8?q?Th=C3=A9o_Zimmermann?= <email address hidden> on 2018-09-25

Fix Sphinx manual targets.

New targets refman, refman-html and refman-pdf.
sphinx keeps its previous meaning (compatibility alias for refman-html).
install-doc-sphinx has been accidentally renamed.

(cherry picked from commit e14757c3779b81a4362a0a88941439adeecdd284)

65a83ab... by =?utf-8?q?Th=C3=A9o_Zimmermann?= <email address hidden> on 2018-09-25

Fix title of Introduction chapter in HTML version.

And location of footnote.

(cherry picked from commit edd0ede5ac057f6a7296351f608f162cd8b0a32b)

031ca3b... by =?utf-8?q?Cl=C3=A9ment_Pit-Claudel?= <email address hidden> on 2018-09-25

[doc] Rename credits-wrapper to credits and credits to credits-contents

This ensures that previous links to 'credits.html' still point to the right page.

(cherry picked from commit 621d1071edd2f243d70c21c1a8f1706325a172eb)

127c506... by =?utf-8?q?Cl=C3=A9ment_Pit-Claudel?= <email address hidden> on 2018-09-25

[doc] Change Sphinx project title back to "Coq"

Use 'The Coq Reference Manual' only in LaTeX.

(cherry picked from commit 846a303c84703da076dfca2e2b1a9bbb70dc697a)