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-06-03
Fix ONLY_WINDOWS in .gitlab-ci.yml.
Théo Zimmermann
2020-06-02
Move CoqIDE to its own folder
Maxime Dénès
2020-06-02
Merge PR #12412: Reduce options passed to workers
Enrico Tassi
2020-06-02
Merge PR #11974: Require in Section: warning is now about fragility not depre...
Emilio Jesus Gallego Arias
2020-06-02
Enforce statically the invariant that a goal comes with its database in eauto.
Pierre-Marie Pédrot
2020-06-02
Simplify Eauto.e_trivial_resolve.
Pierre-Marie Pédrot
2020-06-02
Factor the computation of head constant in Eauto resolution.
Pierre-Marie Pédrot
2020-06-02
Make explicit the computation of lists of goals in eauto.
Pierre-Marie Pédrot
2020-06-02
Some wrapper cleanup around eauto.
Pierre-Marie Pédrot
2020-06-01
Slight improvement in naming existential variables.
Hugo Herbelin
2020-06-01
Merge PR #12396: Release notes 8.12
Emilio Jesus Gallego Arias
2020-06-01
Merge PR #12422: Fixes #12418: an assert false in inference of return clause
Emilio Jesus Gallego Arias
2020-06-01
Merge PR #12431: [ci] Split fiat-crypto into non-OCaml and OCaml
Gaëtan Gilbert
2020-05-31
[ci] Split fiat-crypto into non-OCaml and OCaml
Jason Gross
2020-05-30
Remove info tactic, deprecated in 8.5
Jim Fehrle
2020-05-30
Coq_makefile: adding a dependency of .coqdeps on _CoqProject.
Hugo Herbelin
2020-05-29
Merge PR #12393: [declare] Miscellaneous nits from my main dev tree
Gaëtan Gilbert
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-29
Fixes #12418 (inference of return clause meets assert false).
Hugo Herbelin
2020-05-29
Merge PR #12421: Fixes for compilation without native dynlink
Emilio Jesus Gallego Arias
2020-05-28
Merge PR #12399: Remove the prolog tactic.
Théo Zimmermann
2020-05-28
Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.
Hugo Herbelin
2020-05-28
Fixing compilation with -natdynlink no.
Hugo Herbelin
2020-05-27
Merge PR #12389: Small coq_makefile improvement.
Enrico Tassi
2020-05-27
Adding changelog.
Martin Bodin
2020-05-27
Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters s...
Martin Bodin
2020-05-27
Add more changelog entries which have been backported to v8.12.
Théo Zimmermann
2020-05-27
[changelog/8.12] Wording improvements.
Théo Zimmermann
2020-05-27
[changelog/8.12] Use sections and provide a local TOC.
Théo Zimmermann
2020-05-27
[changelog/8.12] Split misc entries out in more relevant sections.
Théo Zimmermann
2020-05-27
Changelog entries for the 8.12 changes to the reference manual.
Théo Zimmermann
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
[prev]
[next]