index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
changelog
Age
Commit message (
Expand
)
Author
2020-06-05
Add remaining 8.12+beta1 changelog entries.
Théo Zimmermann
2020-06-02
Merge PR #11974: Require in Section: warning is now about fragility not depre...
Emilio Jesus Gallego Arias
2020-06-01
Merge PR #12396: Release notes 8.12
Emilio Jesus Gallego Arias
2020-05-29
Require in Section: warning is now about fragility not deprecation.
Gaëtan Gilbert
2020-05-29
Change log for #12422.
Hugo Herbelin
2020-05-28
Merge PR #12399: Remove the prolog tactic.
Théo Zimmermann
2020-05-27
Adding changelog.
Martin Bodin
2020-05-27
Add more changelog entries which have been backported to v8.12.
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
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-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
Bump minimal versions of refman dependencies.
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
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-15
Changelog entries for #8855.
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
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
2020-05-14
[exn] [tactics] improve backtraces on monadic errors
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #12296: Fixes #12234: wrong environment for Show Proof
Gaëtan Gilbert
2020-05-14
Add a changelog for 8.11.2.
Pierre-Marie Pédrot
2020-05-14
Adding changelog.
Pierre-Marie Pédrot
2020-05-14
Added change log.
Hugo Herbelin
2020-05-14
Add changelog for #12323.
Hugo Herbelin
2020-05-14
Merge PR #12097: Interleave commandline require/set/unset commands
Emilio Jesus Gallego Arias
2020-05-13
Adding change log for #8808.
Hugo Herbelin
2020-05-13
Added change log.
Hugo Herbelin
2020-05-13
Merge PR #11828: [obligations] Deprecated flag cleanup
Gaëtan Gilbert
2020-05-13
Document the changes regarding the order of command-line options.
Théo Zimmermann
2020-05-12
Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.
Jason Gross
2020-05-12
Merge PR #12223: Locating error again in atomic tactics (fixes #12152)
Pierre-Marie Pédrot
[next]