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-03-26
Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sort
Hugo Herbelin
2020-03-26
Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlib
Hugo Herbelin
2020-03-25
Convert Gallina Extensions to use prodn
Jim Fehrle
2020-03-23
Fix levels of `<=?` and `<?` in the stdlib
Jason Gross
2020-03-23
Sorting: Swap the names of Sorted_sort and LocallySorted_sort
Lysxia
2020-03-23
Merge PR #11442: Add module ZifyPow to avoid compatibility issue with 8.11.
Frédéric Besson
2020-03-21
Add module ZifyPow to avoid compatibility issue with 8.11.
Théo Zimmermann
2020-03-21
Reorder the load/require cmd-options and set/unset cmd-options
Lasse Blaauwbroek
2020-03-19
Document all the existing attributes.
Théo Zimmermann
2020-03-19
Merge PR #11760: firstorder: default tactic is “auto with core”
Théo Zimmermann
2020-03-19
Merge PR #11860: [ci] [docker] Update to 4.09.1
Gaëtan Gilbert
2020-03-19
Merge PR #11795: Print implicit arguments in types of references
Hugo Herbelin
2020-03-19
firstorder: default tactic is “auto with core”
Vincent Laporte
2020-03-18
[ci] [docker] Update to 4.09.1
Emilio Jesus Gallego Arias
2020-03-18
Add documentation for the export hint.
Pierre-Marie Pédrot
2020-03-17
Merge PR #11811: Remove a positivity check when Positivity Checking is off
Gaëtan Gilbert
2020-03-14
Merge PR #10858: Implementing postponed constraints in TC resolution
Gaëtan Gilbert
2020-03-13
Implementing postponed constraints in TC resolution
Matthieu Sozeau
2020-03-12
Merge PR #11781: Minor improvements to the unreleased changelog.
Clément Pit-Claudel
2020-03-12
Add changelog
SimonBoulier
2020-03-12
Add changelog entry
SimonBoulier
2020-03-08
Minor improvements to the unreleased changelog.
Théo Zimmermann
2020-03-08
Minor improvements to the unreleased changelog.
Théo Zimmermann
2020-03-08
Merge PR #11740: Ltac2: Add notation for enough and eenough
Pierre-Marie Pédrot
2020-03-05
Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.
Maxime Dénès
2020-03-05
Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...
Pierre-Marie Pédrot
2020-03-05
Merge PR #11602: Adding support for an "only parsing" modifier in "where"-bas...
Pierre-Marie Pédrot
2020-03-04
Merge PR #11429: [zify] several efficiency enhancements
Vincent Laporte
2020-03-04
Adding support for an "only parsing" modifier in "where"-based notations.
Hugo Herbelin
2020-03-03
[loadpath] Rework and simplify ML loadpath handling
Emilio Jesus Gallego Arias
2020-03-03
[zify] efficiency improvements
Frédéric Besson
2020-03-03
Ltac2: Add notation for enough and eenough
Michael Soegtrop
2020-03-03
Update doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst
Hugo Herbelin
2020-03-03
Adding an alias "pose proof (x:=a)" for "pose proof a as x".
Hugo Herbelin
2020-02-28
Deprecating the declaration of arbitrary terms as hints.
Pierre-Marie Pédrot
2020-02-28
Adding change log
Hugo Herbelin
2020-02-27
Merge PR #11650: Set Printing Parens
Emilio Jesus Gallego Arias
2020-02-26
Fix changelog for https://github.com/coq/coq/pull/11686
Maxime Dénès
2020-02-26
Consolidate int63-related notations
Maxime Dénès
2020-02-25
Merge PR #11663: Remove unqualified universe attributes.
Emilio Jesus Gallego Arias
2020-02-24
added changelog
Abhishek Anand (optiplex7010@home)
2020-02-23
Remove unqualified universe attributes.
Théo Zimmermann
2020-02-23
Addressing a changelog comment from Théo Zimmermann.
Hugo Herbelin
2020-02-23
Update doc/changelog/03-notations/11120-master+refactoring-application-printi...
Hugo Herbelin
2020-02-23
Apply and generalize suggestions from Théo.
Hugo Herbelin
2020-02-22
Adding a changelog item.
Hugo Herbelin
2020-02-21
Merge PR #11590: Fixes #9741: only printing notations do not uselessly reserv...
Emilio Jesus Gallego Arias
2020-02-21
Merge PR #11261: Use implicit types for printing (granting wish #10366).
Emilio Jesus Gallego Arias
2020-02-21
Adding changelog for #11590, fixing #9741.
Hugo Herbelin
2020-02-21
Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.
Gaëtan Gilbert
[next]