index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-05-27
Release notes for 8.12.
Théo Zimmermann
2020-05-27
Fix changelog for #11986.
Théo Zimmermann
2020-05-27
Merge PR #12408: Fix output tests for location errors when running in async m...
Emilio Jesus Gallego Arias
2020-05-26
[declare] Split univs_poly_private in close_proof
Emilio Jesus Gallego Arias
2020-05-26
[declare] Factor common universe computation in close proof.
Emilio Jesus Gallego Arias
2020-05-26
[declare] Split univs_deferred in close_proof
Emilio Jesus Gallego Arias
2020-05-26
[declare] Factor out universe computation in close_proof
Emilio Jesus Gallego Arias
2020-05-26
[declare] Nit on errors.
Emilio Jesus Gallego Arias
2020-05-26
[declare] Turn restrict_ucontext hack into an internal parameter
Emilio Jesus Gallego Arias
2020-05-26
[nit] Remove unused exported error message in obligations
Emilio Jesus Gallego Arias
2020-05-26
[declare] Don't expose internal parameter obls
Emilio Jesus Gallego Arias
2020-05-26
[declare] Simplify exported type of definition_entry
Emilio Jesus Gallego Arias
2020-05-26
Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugs
Gaëtan Gilbert
2020-05-26
Fix #12280: do not use xindy to avoid build failures on some machines.
Théo Zimmermann
2020-05-26
Merge PR #12388: Fix an uncaught python exception in timing
Gaëtan Gilbert
2020-05-26
Fix usage of -rifrom, -refrom.
Théo Zimmermann
2020-05-26
Fix worker handling of command-line options that are already included in init...
Théo Zimmermann
2020-05-26
Remove command-line options that do not exist anymore.
Théo Zimmermann
2020-05-25
dev/tools/make-changelog.sh now asks about fixed bugs
Jason Gross
2020-05-25
Merge PR #12366: Delay evaluating arguments of the "exists" tactic
Pierre-Marie Pédrot
2020-05-25
Merge PR #12344: Cleanup noisy prefixes
Pierre-Marie Pédrot
2020-05-25
Fix output tests for location errors when running in async mode.
Théo Zimmermann
2020-05-25
Merge PR #12403: Fix hyperlinks in changes.rst
Théo Zimmermann
2020-05-25
Fix #12406: fix Coq type error in dependent induction's Ltac
Paolo G. Giarrusso
2020-05-25
Add a changelog.
Pierre-Marie Pédrot
2020-05-25
Remove the prolog tactic.
Pierre-Marie Pédrot
2020-05-24
Fix hyperlinks in changes.rst
Matthew Dempsky
2020-05-24
Merge PR #12392: [backport-pr] Select correct remote of the master branch.
Jason Gross
2020-05-24
Merge PR #12379: Omit voluminous Latex warnings
Théo Zimmermann
2020-05-23
[dev/tools] Fix #12314: do not die silently if branch has no remote.
Théo Zimmermann
2020-05-22
[backport-pr] Select correct remote of the master branch.
Théo Zimmermann
2020-05-22
Merge PR #12076: [coqchk] Fix #5030 (coqchk reports names from opaque modules...
Pierre-Marie Pédrot
2020-05-22
[coqchk] Improve previous heuristic.
Pierre Roux
2020-05-22
[coqchk] Add test
Pierre Roux
2020-05-22
[coqchk] Fix #5030
Pierre Roux
2020-05-22
[coqchk] Change list to set
Pierre Roux
2020-05-22
Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...
Pierre-Marie Pédrot
2020-05-22
Merge PR #11986: [primitive floats] Add low level printing
Pierre-Marie Pédrot
2020-05-21
Fix an uncaught python exception in timing
Jason Gross
2020-05-21
Merge PR #12371: [obligations] Minor refactoring
Gaëtan Gilbert
2020-05-21
Merge PR #12368: Print a newline at the end of timing tables
Gaëtan Gilbert
2020-05-21
Merge PR #12364: [ci] [docker] Bump ocamlformat and dune
Gaëtan Gilbert
2020-05-21
Merge PR #12358: [topfmt] Set formatter + flush fix
Gaëtan Gilbert
2020-05-21
Merge PR #12316: Use pagination in fetching the number of reviews
Gaëtan Gilbert
2020-05-20
Print a newline at the end of timing tables
Jason Gross
2020-05-20
[merge-pr] Use a simpler method to get all pages
Jason Gross
2020-05-20
[merge-pr.sh] Follow next links instead
Jason Gross
2020-05-20
Use pagination in fetching the number of reviews
Jason Gross
2020-05-20
Omit volumnious Latex messages
Jim Fehrle
2020-05-20
Merge PR #12377: Adapt the documentation to the move from Gitter to Zulip.
Clément Pit-Claudel
[prev]
[next]