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-09-23
Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)
coqbot-app[bot]
2020-09-23
Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of quotatio...
Pierre-Marie Pédrot
2020-09-23
Merge PR #12847: Tactics inversion and replace work with eq in type
Pierre-Marie Pédrot
2020-09-22
Merge PR #13067: Setting default value for Display Parentheses off in CoqIDE
coqbot-app[bot]
2020-09-22
Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applica...
coqbot-app[bot]
2020-09-22
Adding change log for #12794 and #13067.
Hugo Herbelin
2020-09-22
Adding change log for #13028.
Hugo Herbelin
2020-09-21
Make print-pretty-timed robust against non-output-sync logs
Jason Gross
2020-09-17
[build] Don't link `num` anymore in Coq
Emilio Jesus Gallego Arias
2020-09-15
Adding change log for #13026.
Hugo Herbelin
2020-09-15
Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"
Pierre-Marie Pédrot
2020-09-14
Remove deprecated Extraction Language command value "Ocaml"
Jim Fehrle
2020-09-14
[ci] [docker] Up testing to OCaml 4.11.1
Emilio Jesus Gallego Arias
2020-09-11
Rename Numeral Notation command to Number Notation
Pierre Roux
2020-09-11
Minimal changes to make the refman compatible with Sphinx 3.
Théo Zimmermann
2020-09-10
Merge PR #12998: changelog entry for 12857
coqbot-app[bot]
2020-09-10
Update doc/changelog/06-ssreflect/12857-changelog-for-12857.rst
Enrico Tassi
2020-09-09
Merge PR #12094: Extend app_inj_tail and other list lemmas
Hugo Herbelin
2020-09-09
changelog entry for 12857
Enrico Tassi
2020-09-09
Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...
Pierre-Marie Pédrot
2020-09-08
Remove deprecated tactic cutrewrite.
Théo Zimmermann
2020-09-07
Refine test for unresolved evars: not reachable from initial evars
Matthieu Sozeau
2020-09-07
Add changelog entry
Edward Wang
2020-09-02
Adding change log for #12960.
Hugo Herbelin
2020-08-27
[zarith] Changelog
Emilio Jesus Gallego Arias
2020-08-27
Merge PR #12862: [coqchk] Look inside inner modules as well
Pierre-Marie Pédrot
2020-08-25
Require NsatzTactic: nsatz support for Z and Q
Jason Gross
2020-08-25
Merge PR #12801: Put cyclic numbers in sort Set instead of Type
Anton Trunov
2020-08-24
Put cyclic numbers in sort Set instead of Type
Vincent Semeria
2020-08-24
Merge PR #12738: Fix subject reduction VS cumulative inductives and function eta
coqbot
2020-08-24
Merge PR #12864: Improve `make approve-output`
Gaëtan Gilbert
2020-08-20
Adding change log for PR #12816.
Hugo Herbelin
2020-08-20
Merge PR #12756: Do not refresh the names of implicit arguments.
Maxime Dénès
2020-08-19
Improve `make approve-output`
Jason Gross
2020-08-19
[coqchk] Look inside inner modules as well
Jason Gross
2020-08-19
Do not refresh the names of implicit arguments.
Jasper Hugunin
2020-08-18
Fix subject reduction VS cumulative inductives and function eta
Gaëtan Gilbert
2020-08-18
Adding change log for #12847.
Hugo Herbelin
2020-08-13
Merge PR #12799: [stdlib] [List] Additional statements about List.repeat
Anton Trunov
2020-08-13
Merge PR #12716: deprecate prod_curry and prod_uncurry
Anton Trunov
2020-08-13
Merge PR #12556: Bring Float notations in line with stdlib
Hugo Herbelin
2020-08-12
Additional statements about List.repeat
Olivier Laurent
2020-08-11
add deprecation to changelog
Yishuai Li
2020-08-09
Bring Int63 notations into line with stdlib
Jason Gross
2020-08-09
Bring Float notations in line with stdlib
Jason Gross
2020-07-29
coqdoc: Fix the “details” environment
Thomas Letan
2020-07-28
Merge PR #12754: Fixes #12752: applying symbol escaping in coqdoc index
Li-yao Xia
2020-07-24
Adding change log for #12754.
Hugo Herbelin
2020-07-23
[changelog] Incorporate hanging changelog entry for 8.12+beta1
Emilio Jesus Gallego Arias
2020-07-23
[changelog] Fix hanging file extension.
Emilio Jesus Gallego Arias
[next]