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-12-04
[rm] update git commands to push tags
Enrico Tassi
2020-11-27
Merge PR #13449: [RM] script to notify "platform" projects to tag
coqbot-app[bot]
2020-11-27
Merge PR #13482: Improved error message on nested proofs
coqbot-app[bot]
2020-11-27
[RM] script to notify "platform" projects to tag
Enrico Tassi
2020-11-27
Merge PR #13473: Testing {in _, _} and {pred _} from ssrbool
coqbot-app[bot]
2020-11-27
Improved error message on nested proofs
Fabian Kunze
2020-11-27
Merge PR #13468: Fixes #13456: regression in tactic exists which started to c...
Pierre-Marie Pédrot
2020-11-27
Merge PR #13457: [RM] Update magicno & compat
coqbot-app[bot]
2020-11-27
Merge PR #13491: Reactivate test-suite on MacOS X, accidently merged in #13476
coqbot-app[bot]
2020-11-26
Reactivate test-suite on MacOS X, accidently merged in #13476.
Hugo Herbelin
2020-11-26
Fixes #13456: regression where tactic exists started to check evars increment...
Hugo Herbelin
2020-11-26
Merge PR #13467: [ci] add job for interval
coqbot-app[bot]
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
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]
[next]