index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
Age
Commit message (
Expand
)
Author
2020-05-27
Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters s...
Martin Bodin
2020-05-27
Add 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-27
Changelog entries for the 8.12 changes to the reference manual.
Théo Zimmermann
2020-05-27
Release notes for 8.12.
Théo Zimmermann
2020-05-27
Fix changelog for #11986.
Théo Zimmermann
2020-05-26
Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugs
Gaëtan Gilbert
2020-05-26
Fix #12280: do not use xindy to avoid build failures on some machines.
Théo Zimmermann
2020-05-26
Merge PR #12388: Fix an uncaught python exception in timing
Gaëtan Gilbert
2020-05-25
dev/tools/make-changelog.sh now asks about fixed bugs
Jason Gross
2020-05-25
Merge PR #12366: Delay evaluating arguments of the "exists" tactic
Pierre-Marie Pédrot
2020-05-25
Add a changelog.
Pierre-Marie Pédrot
2020-05-24
Fix hyperlinks in changes.rst
Matthew Dempsky
2020-05-22
[coqchk] Fix #5030
Pierre Roux
2020-05-22
Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...
Pierre-Marie Pédrot
2020-05-22
Merge PR #11986: [primitive floats] Add low level printing
Pierre-Marie Pédrot
2020-05-21
Fix an uncaught python exception in timing
Jason Gross
2020-05-21
Merge PR #12368: Print a newline at the end of timing tables
Gaëtan Gilbert
2020-05-20
Print a newline at the end of timing tables
Jason Gross
2020-05-19
Delay evaluating arguments of the "exists" tactic
Attila Gáspár
2020-05-19
[topfmt] Set formatter + flush fix
Emilio Jesus Gallego Arias
2020-05-19
[primitive floats] Add low level hexadecimal printing
Pierre Roux
2020-05-18
Use the new gdef alt-text feature in the refman.
Théo Zimmermann
2020-05-18
Support :gdef:`text <term>` syntax (adding "<term>")
Jim Fehrle
2020-05-18
Bump minimal versions of refman dependencies.
Théo Zimmermann
2020-05-18
Update to 8.13.
Théo Zimmermann
2020-05-17
Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place ...
Jason Gross
2020-05-17
Ltac2: add notations for eval cbv in ... and other in place reductions
Michael Soegtrop
2020-05-16
Merge PR #12288: Prove that classical reals implement constructive reals.
Michael Soegtrop
2020-05-16
Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.
Emilio Jesus Gallego Arias
2020-05-16
Merge PR #12330: Add redirects for HTML pages that were moved.
Clément Pit-Claudel
2020-05-16
Merge PR #8855: More search options
Emilio Jesus Gallego Arias
2020-05-16
Merge PR #12277: Checking validity of coqdoc file name (fixes #12265)
Théo Zimmermann
2020-05-16
Fix note on implicit arguments in doc of functional induction.
Théo Zimmermann
2020-05-16
Fix #11761: Functional Induction throws unrecoverable error.
Pierre Courtieu
2020-05-16
Prove that classical reals implement constructive reals. Also move sums, min ...
Vincent Semeria
2020-05-16
Add redirects for HTML pages that were moved.
Théo Zimmermann
2020-05-15
Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into mul...
Clément Pit-Claudel
2020-05-15
Changelog entries for #8855.
Théo Zimmermann
2020-05-15
Document new Search features.
Théo Zimmermann
2020-05-15
Move SSR's Search to a new plugin and deprecate it.
Théo Zimmermann
2020-05-15
Update docgram following #12122 and #12229.
Théo Zimmermann
2020-05-15
Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with impli...
Emilio Jesus Gallego Arias
2020-05-15
Merge PR #11948: Hexadecimal numerals
Hugo Herbelin
2020-05-15
Merge PR #11755: [exn] [tactics] improve backtraces on monadic errors
Pierre-Marie Pédrot
2020-05-15
Fix typo.
Théo Zimmermann
2020-05-15
Merge PR #11992: do not re-export ListNotations from Program
Anton Trunov
2020-05-14
Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...
Hugo Herbelin
[prev]
[next]