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-11-26
[ci] interval, disable native-compute
Enrico Tassi
2020-11-26
[ci] coquelicot, depend on ssr proper
Enrico Tassi
2020-11-26
[ci] avoid always rebuilding jobs that use remake
Enrico Tassi
2020-11-26
[ci] separate oddorder and fourcolor from mathcomp
Enrico Tassi
2020-11-26
Merge PR #13415: Separate interning and pretyping of universes
coqbot-app[bot]
2020-11-26
Merge PR #13481: [ci] elpi 1.12
coqbot-app[bot]
2020-11-26
Merge PR #13476: MacOS X install: accepting both dylib and so extensions for ...
coqbot-app[bot]
2020-11-26
[ci] bump elpi to 1.12.0
Enrico Tassi
2020-11-26
[ci] add job for interval
Enrico Tassi
2020-11-26
[ci] coquelicot, run make install
Enrico Tassi
2020-11-26
Merge PR #13379: Add a new evar source to refer to evars which are types of e...
coqbot-app[bot]
2020-11-26
extracting API for comparing universes of constants/inductives/constructors
beta
2020-11-26
Merge PR #13464: [CI] Compcert uses system libs
coqbot-app[bot]
2020-11-25
Merge PR #13447: Remove unused parsing code
coqbot-app[bot]
2020-11-25
tmp deactivation test-suite
Hugo Herbelin
2020-11-25
MacOS X install: accepting both dylib and so extensions for gtk immodules.
Hugo Herbelin
2020-11-25
[docker] don't install ocamlformat
Enrico Tassi
2020-11-25
[ci] make compcert use flocq and menhir
Enrico Tassi
2020-11-25
[ci] job for menhir
Enrico Tassi
2020-11-25
Merge PR #13228: [micromega] Performance of lia
Pierre-Marie Pédrot
2020-11-25
Testing {in _, _} and {pred _} from ssrbool
Cyril Cohen
2020-11-25
Overlays for #13415
Gaëtan Gilbert
2020-11-25
Changelog for #13415
Gaëtan Gilbert
2020-11-25
Add tests for #13303
Gaëtan Gilbert
2020-11-25
Clean UnivBinders test
Gaëtan Gilbert
2020-11-25
Separate interning and pretyping of universes
Gaëtan Gilbert
2020-11-25
Reserve "sort_expr" for uninterned universes
Gaëtan Gilbert
2020-11-25
Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bug
coqbot-app[bot]
2020-11-25
Merge PR #13405: Alternative implementation of the Micromega persistent cache
Vincent Laporte
2020-11-25
Merge PR #13343: Update syntax in auto.rst chapter
coqbot-app[bot]
2020-11-24
Convert auto chapter to prodn
Jim Fehrle
2020-11-24
[ci] variable CI_INSTALL_DIR to use with --prefix
Enrico Tassi
2020-11-24
Add a changelog.
Pierre-Marie Pédrot
2020-11-24
Keep accessed objects in memory in Persistent_cache.
Pierre-Marie Pédrot
2020-11-24
Regenerate the csdp cache for the test-suite.
Pierre-Marie Pédrot
2020-11-24
Alternative implementation of the Micromega persistent cache.
Pierre-Marie Pédrot
2020-11-24
Preserve sharing in the Micromega cache.
Pierre-Marie Pédrot
2020-11-24
Add an explicit signature to the MakeCache functor in Micromega.
Pierre-Marie Pédrot
2020-11-24
Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a ...
coqbot-app[bot]
2020-11-24
Fixing [dup] and [swap]
Cyril Cohen
2020-11-24
Merge PR #13466: Fix linter: incorrect commit was picked in CI
coqbot-app[bot]
2020-11-24
Merge PR #13455: Fix comparison of extracted array literals
coqbot-app[bot]
2020-11-24
Add a new evar source to refer to evars which are types of evars.
Hugo Herbelin
2020-11-24
Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction o...
coqbot-app[bot]
2020-11-24
Merge PR #13420: Modular printing algorithm for bench/render_results.
coqbot-app[bot]
2020-11-24
Merge PR #13411: Rename the confusing neutral annotation in CClosure.
coqbot-app[bot]
2020-11-24
Fix linter: incorrect commit was picked in CI
Gaëtan Gilbert
2020-11-24
update default.nix
Enrico Tassi
2020-11-23
Add COPYALL and APPENDALL edit ops, drop unneeded code
Jim Fehrle
2020-11-23
Update compat infrastructure for 8.14
Enrico Tassi
[prev]
[next]