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
2021-03-06
Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoids
Pierre-Marie Pédrot
2021-03-06
Merge PR #13236: Add a type of format strings to Ltac2.
Michael Soegtrop
2021-03-05
Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)
Pierre-Marie Pédrot
2021-03-04
Properly support nested timeouts
Lasse Blaauwbroek
2021-03-04
[doc] changelog entry
Enrico Tassi
2021-03-04
Fix #12011 ssreflect "rewrite in" with setoids
Gaëtan Gilbert
2021-03-03
[build] Split stdlib to it's own opam package.
Emilio Jesus Gallego Arias
2021-02-28
Merge PR #13853: Delay the dynamic linking of native-code libraries until nat...
Pierre-Marie Pédrot
2021-02-27
Merge PR #13876: [coqc] Don't allow to pass more than one file to coqc
coqbot-app[bot]
2021-02-27
Add changelog
Pierre Roux
2021-02-26
[coqc] Don't allow to pass more than one file to coqc
Emilio Jesus Gallego Arias
2021-02-26
Signed primitive integers
Ana
2021-02-26
Delay the dynamic linking of native-code libraries until native_compute is ca...
Guillaume Melquiond
2021-02-25
Merge PR #13202: Infrastructure for fine-grained debug flags
coqbot-app[bot]
2021-02-25
Merge PR #13080: Ascii: add leb and ltb
coqbot-app[bot]
2021-02-24
Infrastructure for fine-grained debug flags
Maxime Dénès
2021-02-22
changelog for 8.13.1
Enrico Tassi
2021-02-20
Update doc/changelog/01-kernel/13867-changelog-for-13867.rst
Enrico Tassi
2021-02-20
add changelog for 13867
Enrico Tassi
2021-02-09
Merge PR #13822: Remove deprecated command line arguments
coqbot-app[bot]
2021-02-04
Changelog for #13822
Gaëtan Gilbert
2021-02-01
Add changelog entry
slrnsc
2021-01-29
add changelog
Olivier Laurent
2021-01-28
Merge PR #13781: [micromega] Deprecate hopefully useless options and flags
coqbot-app[bot]
2021-01-28
Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)
coqbot-app[bot]
2021-01-26
Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)
coqbot-app[bot]
2021-01-25
Remove the SearchHead command
Jim Fehrle
2021-01-25
Remove the Hide Obligations flag
Jim Fehrle
2021-01-25
Update doc/changelog/04-tactics/13781-deprecate_micromega_options.rst
Frédéric Besson
2021-01-24
Merge PR #13762: Remove double induction tactic
Pierre-Marie Pédrot
2021-01-22
changelog
BESSON Frederic
2021-01-22
Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)
Pierre-Marie Pédrot
2021-01-22
Add documentation for Ltac2 Printf.
Pierre-Marie Pédrot
2021-01-20
Remove double induction tactic
Jim Fehrle
2021-01-19
Remove Add InjTyp and 10 other micromega commands
Jim Fehrle
2021-01-19
Remove convert_concl_no_check
Jim Fehrle
2021-01-19
Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)
Pierre-Marie Pédrot
2021-01-19
Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction pat...
Pierre-Marie Pédrot
2021-01-18
Adding changelog for #13512.
Hugo Herbelin
2021-01-18
Support locality attributes for Hint Rewrite (including export)
Gaëtan Gilbert
2021-01-18
Add changelog
Pierre Roux
2021-01-07
Use nat_or_var for fail/gfail
Jim Fehrle
2021-01-07
Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ...
Pierre-Marie Pédrot
2021-01-07
Merge PR #13715: [micromega] Add missing support for `implb`
Vincent Laporte
2021-01-06
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-m...
coqbot-app[bot]
2021-01-06
[micromega] Add missing support for `implb`
BESSON Frederic
2021-01-04
Document the change of case representation.
Pierre-Marie Pédrot
2021-01-04
Changelog for 8.13.0
Enrico Tassi
2021-01-02
Deprecate "at ... with ..." in change tactic
Jim Fehrle
2020-12-16
Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ta...
Pierre-Marie Pédrot
[prev]
[next]