index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-04-08
Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.
Pierre-Marie Pédrot
2019-04-08
Don't store closures in summary (reduction effects)
Gaëtan Gilbert
2019-04-08
Merge PR #9915: Remove cache in Heads
Enrico Tassi
2019-04-08
coq_makefile install target: error if any file is missing
Gaëtan Gilbert
2019-04-08
Merge PR #9900: [native compiler] Fix critical bug with stuck primitive proje...
Pierre-Marie Pédrot
2019-04-06
Merge PR #9924: Fix numeral notations test in async mode.
Emilio Jesus Gallego Arias
2019-04-06
Fix numeral notations test in async mode.
Gaëtan Gilbert
2019-04-06
Merge PR #9923: [ci/deploy] Fix branch creation when pushing to coq/coq-on-ca...
Emilio Jesus Gallego Arias
2019-04-06
Fix pretty-printing of primitive integers
Erik Martin-Dorel
2019-04-06
[ci/deploy] Fix branch creation when pushing to coq/coq-on-cachix.
Théo Zimmermann
2019-04-05
[native compiler] Fix critical bug with primitive projections
Maxime Dénès
2019-04-05
[native compiler] Normalize before destructuring sort
Maxime Dénès
2019-04-05
[api] [proofs] Remove dependency of proofs on interp.
Emilio Jesus Gallego Arias
2019-04-05
Merge PR #9685: [vernac] Small cleanup to remove assert false.
Vincent Laporte
2019-04-05
Remove cache in Heads
Maxime Dénès
2019-04-05
Merge pull request coq/ltac2#116 from proux01/master-parsing-decimal
Pierre-Marie Pédrot
2019-04-05
Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)
Emilio Jesus Gallego Arias
2019-04-04
Update CHANGES.md
Pierre Roux
2019-04-04
Adapt to coq/coq#8764
Pierre Roux
2019-04-04
Merge PR #9904: [CI] Fix build of math-comp dependencies
Gaëtan Gilbert
2019-04-04
[CI] Fix build of math-comp dependencies
Maxime Dénès
2019-04-04
Merge PR #9901: [dune] Fix include object dirs.
Théo Zimmermann
2019-04-04
[dune] Fix include object dirs.
Emilio Jesus Gallego Arias
2019-04-04
Merge PR #9881: Protect some I/O routines from SIGALRM
Emilio Jesus Gallego Arias
2019-04-03
Merge PR #9890: Improve coqchk -norec perf by not checking for ill-formed dat...
Pierre-Marie Pédrot
2019-04-03
Merge PR #9804: CI: Use job-local timeout for build-template and test-suite-t...
Emilio Jesus Gallego Arias
2019-04-03
Merge PR #9861: [program] Allow evars in type of fixpoints.
Gaëtan Gilbert
2019-04-03
Protect some I/O routines from SIGALRM
Maxime Dénès
2019-04-03
Merge PR #9078: Provide a faster bound name generation algorithm through a flag
Vincent Laporte
2019-04-03
Merge PR #9896: Minor correction to numeral notations doc
Théo Zimmermann
2019-04-03
Merge PR #8638: Remove -compat 8.7
Théo Zimmermann
2019-04-03
Minor correction to numeral notations doc
Jason Gross
2019-04-02
Merge PR #9668: Consolidate credits and changelog information in a single place.
Clément Pit-Claudel
2019-04-02
[ssr] rewrite takes optional function to make the new valued of the redex
Enrico Tassi
2019-04-02
[ssr] implement "under i: ext_lemma" by rewrite rule
Enrico Tassi
2019-04-02
[ssr] under: Add opaque modules for tagging and notation support
Erik Martin-Dorel
2019-04-02
[ssr] fix implementation of refine ~first_goes_last
Enrico Tassi
2019-04-02
[ssr] clean up type declaration of ssrrewritetac
Enrico Tassi
2019-04-02
[ssr] move is_ind/constructor_ref to ssrcommon
Enrico Tassi
2019-04-02
[ssr] under: rewrite takes an optional bool arg
Erik Martin-Dorel
2019-04-02
CI: Use job-local timeout for build-template and test-suite-template
Gaëtan Gilbert
2019-04-02
Merge pull request coq/ltac2#118 from vbgl/rm-hardwired-hint-db
Pierre-Marie Pédrot
2019-04-02
Merge PR #8984: Declare initial hint databases in prelude
Pierre-Marie Pédrot
2019-04-02
coqchk: use unsafe marshal for dependencies of -norec libraries
Gaëtan Gilbert
2019-04-02
coqchk: don't marshal opaques for dependencies of -norec libraries
Gaëtan Gilbert
2019-04-02
coqchk: do not validate dependencies of -norec libraries
Gaëtan Gilbert
2019-04-02
Remove -compat 8.7
Jason Gross
2019-04-02
Merge PR #9875: [doc] Add a note about Dune support to the manual.
Théo Zimmermann
2019-04-02
Merge pull request coq/ltac2#117 from ejgallego/opam_update
Pierre-Marie Pédrot
2019-04-02
[opam] Update file to newer format and build system.
Emilio Jesus Gallego Arias
[prev]
[next]