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-03
Fixes in the summary by Jim Fehrle
Matthieu Sozeau
2020-12-03
Changes without PR references fixes
Matthieu Sozeau
2020-12-03
Apply suggestions from @jfehrle code review
Matthieu Sozeau
2020-12-03
[changelog] update markup
Enrico Tassi
2020-12-03
Add an anchor in syntax-extensions
Matthieu Sozeau
2020-12-03
Changes for Coq 8.13
Matthieu Sozeau
2020-12-03
Merge PR #13554: Split long lines in errors and warning index
coqbot-app[bot]
2020-12-02
Split long lines in errors and warning index
Jim Fehrle
2020-12-02
Merge PR #13275: Put all Int63 primitives in a separate file
Vincent Laporte
2020-12-02
Merge PR #13471: gitlab CI: remove redundant "dependencies" info
coqbot-app[bot]
2020-12-02
Merge PR #13543: Fix a bug in funind.
coqbot-app[bot]
2020-12-02
gitlab CI: remove redundant "dependencies" info
Gaëtan Gilbert
2020-12-02
Merge PR #13472: [ci] Add job for gappa
coqbot-app[bot]
2020-12-02
Put all Int63 primitives in a separate file
Pierre Roux
2020-12-01
Fix a bug in funind.
Pierre-Marie Pédrot
2020-12-01
Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0
coqbot-app[bot]
2020-12-01
Merge PR #13526: dune: Don't echo "$(pwd)" when creating the shims
coqbot-app[bot]
2020-12-01
Merge PR #13531: [kernel]Use ~l2r:true to restore previous order of unfolding
coqbot-app[bot]
2020-12-01
Added comment about l2r in check_correct_arity
Gaëtan Gilbert
2020-12-01
Use ~l2r:true to restore previous order of unfolding when typing predicates o...
Matthieu Sozeau
2020-11-30
[ci] add job for gappa
Enrico Tassi
2020-11-30
[docker] install boost, mpfr, flex, bison, autoconf-archive
Enrico Tassi
2020-11-30
dune: Don't echo "$(pwd)" when creating the shims
Gaëtan Gilbert
2020-11-30
Merge PR #13506: Micro-optimizations of the tight loop in Hashset.
coqbot-app[bot]
2020-11-30
Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumu...
coqbot-app[bot]
2020-11-29
Merge PR #13510: Add missing print registration for wit_nat_or_var
coqbot-app[bot]
2020-11-29
Micro-optimizations of the tight loop in Hashset.
Pierre-Marie Pédrot
2020-11-29
Merge PR #13514: Fixing printing of apply in (continuation of #12246)
Pierre-Marie Pédrot
2020-11-29
Backport ssrbool lemmas from MathComp 1.12.0
Kazuhiko Sakaguchi
2020-11-29
Fixing printing of apply in (continuation of #12246).
Hugo Herbelin
2020-11-28
Add missing print registration for wit_nat_or_var
Jim Fehrle
2020-11-28
Merge PR #13502: A small fix for freshness in the `change` tactic
coqbot-app[bot]
2020-11-28
Merge PR #13487: CI: Use hash of dockerfile in CACHEKEY
coqbot-app[bot]
2020-11-28
Merge PR #13479: extracting API for comparing universes of constants/inductiv...
coqbot-app[bot]
2020-11-28
Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."
coqbot-app[bot]
2020-11-27
Merge PR #12586: [declare] Allow custom typing flags when declaring constants.
coqbot-app[bot]
2020-11-27
[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ...
Matthieu Sozeau
2020-11-27
A small fix for freshness in the `change` tactic
Jasper Hugunin
2020-11-27
Merge PR #13483: Fix #13283: improved error on `clear implicit` flag
coqbot-app[bot]
2020-11-27
Merge PR #13449: [RM] script to notify "platform" projects to tag
coqbot-app[bot]
2020-11-27
Revert "Remove deprecated tactic cutrewrite."
Théo Zimmermann
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
Fix #13283: improved error on `clear implicit` flag
Fabian Kunze
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
[attributes] [typing] Rename `typing` to `bypass_check`
Emilio Jesus Gallego Arias
[next]