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-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
2020-07-23
[changelog] Latest changes backported to 8.12 branch.
Emilio Jesus Gallego Arias
2020-07-23
Merge PR #12678: Tweak the warning for arbitrary term hints.
Emilio Jesus Gallego Arias
2020-07-17
Add a changelog.
Pierre-Marie Pédrot
2020-07-17
Merge PR #12683: Fixes #12682: printing bug with recursive notations for n-ar...
Emilio Jesus Gallego Arias
2020-07-17
Add changelog.
Pierre-Marie Pédrot
2020-07-12
Adding change log.
Hugo Herbelin
2020-07-10
Add changelog.
Pierre-Marie Pédrot
2020-07-08
Adding change log.
Hugo Herbelin
2020-07-06
Merge PR #11604: Primitive persistent arrays
Pierre-Marie Pédrot
2020-07-06
Primitive persistent arrays
Maxime Dénès
2020-07-05
Merge PR #12594: Fix ltac2 type parameters
Michael Soegtrop
2020-07-05
Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -I
Pierre-Marie Pédrot
2020-07-03
Fix #11121: Simultaneous definition of term and notation in custom grammar
Maxime Dénès
2020-07-03
Merge PR #10390: UIP in SProp
Maxime Dénès
2020-07-02
Merge PR #12572: Correctly classify variables as being unfoldable in dnet pat...
Gaëtan Gilbert
2020-07-01
Add a changelog.
Pierre-Marie Pédrot
2020-07-01
UIP in SProp
Gaëtan Gilbert
2020-07-01
Remove deprecated (in 8.8 #6277) coqchk -I
Gaëtan Gilbert
2020-06-29
Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_list
Pierre-Marie Pédrot
2020-06-24
[test-suite] Fix dependencies of modules/ files
Jason Gross
2020-06-23
Correctly classify variables as being unfoldable in dnet patterns.
Pierre-Marie Pédrot
2020-06-23
Merge PR #12562: CoqIDE: accept to open files with invalid names
Michael Soegtrop
2020-06-22
CoqIDE: accept to open files with invalid names
Vincent Laporte
2020-06-20
Add a pre-hook mechanism for the `zify` tactic
Kazuhiko Sakaguchi
2020-06-18
Fix #12228 negative integers not accepted in ltac integer_list
Pierre Roux
2020-06-14
[micromega] native support for boolean operators
Frédéric Besson
2020-06-11
Merge PR #12423: Remove info tactic, deprecated in 8.5
Pierre-Marie Pédrot
2020-06-10
Update changelog for 8.12+beta1.
Théo Zimmermann
2020-06-09
Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.leb
Guillaume Melquiond
2020-06-09
CReal: changed epsilon for modulus of convergence from 1/n to 2^z
Michael Soegtrop
2020-06-08
Fix 12483
Pierre Roux
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-30
Remove info tactic, deprecated in 8.5
Jim Fehrle
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
[next]