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-10-26
Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...
coqbot-app[bot]
2020-10-22
Merge PR #11924: Add style for smallcaps.
coqbot-app[bot]
2020-10-20
Add some missing smallcaps.
Théo Zimmermann
2020-10-20
[zify] Add support for Int63.int
Frédéric Besson
2020-10-16
Add change log for #13166.
Hugo Herbelin
2020-10-12
Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol
coqbot-app[bot]
2020-10-12
Merge PR #12449: Minimize Prop <= i to i := Set
coqbot-app[bot]
2020-10-10
Adding change log for #12950.
Hugo Herbelin
2020-10-09
Add an XML message for "Show Proof Diffs"
Jim Fehrle
2020-10-09
Minimize Prop <= i to i := Set
Gaëtan Gilbert
2020-10-05
Change log for #12768.
Hugo Herbelin
2020-10-05
Document the removal of forward class hints.
Théo Zimmermann
2020-10-04
Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...
coqbot-app[bot]
2020-10-04
Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."
Jim Fehrle
2020-09-28
Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lon...
coqbot-app[bot]
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-09-02
Adding change log for #12946.
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
[next]