aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-03Implement suggestions by Théo ZimmermannMatthieu Sozeau
2020-12-03Apply suggestions from code reviewMatthieu Sozeau
Co-authored-by: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-12-03Apply suggestions from code reviewEnrico Tassi
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Update doc/sphinx/changes.rstMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Fixes in the summary by Jim FehrleMatthieu Sozeau
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-12-03Changes without PR references fixesMatthieu Sozeau
2020-12-03Apply suggestions from @jfehrle code reviewMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Add an anchor in syntax-extensionsMatthieu Sozeau
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-12-03Merge PR #13554: Split long lines in errors and warning indexcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-02Split long lines in errors and warning indexJim Fehrle
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Merge PR #13471: gitlab CI: remove redundant "dependencies" infocoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-02Merge PR #13543: Fix a bug in funind.coqbot-app[bot]
Reviewed-by: Matafou
2020-12-02gitlab CI: remove redundant "dependencies" infoGaëtan Gilbert
When we started using "needs" for the acyclic graph scheduling we needed to duplicate dependencies and needs (I forgot if it was documented or just buggy). Nowadays gitlab doc https://docs.gitlab.com/ee/ci/yaml/#needs says >In GitLab 12.6 and later, you can’t combine the dependencies keyword with needs to control artifact downloads in jobs. dependencies is still valid in jobs that do not use needs. Some jobs in stage-1 had "dependencies: []" without a corresponding "needs", not sure why as the only job in a previous stage is docker-boot which has no artifacts to skip. We don't want "needs: []" as that would fail to wait for the docker image, so we just have nothing instead.
2020-12-02Merge PR #13472: [ci] Add job for gappacoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: ejgallego
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
2020-12-01Fix a bug in funind.Pierre-Marie Pédrot
It was generating a completely nonsense case branch, but for some reason the proof still went trough.
2020-12-01Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0coqbot-app[bot]
Reviewed-by: gares
2020-12-01Merge PR #13526: dune: Don't echo "$(pwd)" when creating the shimscoqbot-app[bot]
Reviewed-by: ejgallego
2020-12-01Merge PR #13531: [kernel]Use ~l2r:true to restore previous order of unfolding coqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: ppedrot
2020-12-01Added comment about l2r in check_correct_arityGaëtan Gilbert
2020-12-01Use ~l2r:true to restore previous order of unfolding when typing predicates ↵Matthieu Sozeau
of cases.
2020-11-30[ci] add job for gappaEnrico Tassi
2020-11-30[docker] install boost, mpfr, flex, bison, autoconf-archiveEnrico Tassi
2020-11-30dune: Don't echo "$(pwd)" when creating the shimsGaëtan Gilbert
AFAICT `echo "$(pwd)"` is unsound for the dune cache when called from different paths (typically different git worktrees).
2020-11-30Merge PR #13506: Micro-optimizations of the tight loop in Hashset.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for ↵coqbot-app[bot]
cumulative inductive types Reviewed-by: SkySkimmer
2020-11-29Merge PR #13510: Add missing print registration for wit_nat_or_varcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-29Micro-optimizations of the tight loop in Hashset.Pierre-Marie Pédrot
2020-11-29Merge PR #13514: Fixing printing of apply in (continuation of #12246)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-29Backport ssrbool lemmas from MathComp 1.12.0Kazuhiko Sakaguchi
2020-11-29Fixing printing of apply in (continuation of #12246).Hugo Herbelin
2020-11-28Add missing print registration for wit_nat_or_varJim Fehrle
2020-11-28Merge PR #13502: A small fix for freshness in the `change` tacticcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-28Merge PR #13487: CI: Use hash of dockerfile in CACHEKEYcoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares
2020-11-28Merge PR #13479: extracting API for comparing universes of ↵coqbot-app[bot]
constants/inductives/constructors Reviewed-by: SkySkimmer
2020-11-28Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."coqbot-app[bot]
Reviewed-by: gares
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: herbelin Ack-by: jfehrle
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ↵Matthieu Sozeau
types
2020-11-27A small fix for freshness in the `change` tacticJasper Hugunin
2020-11-27Merge PR #13483: Fix #13283: improved error on `clear implicit` flagcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-27Merge PR #13449: [RM] script to notify "platform" projects to tagcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
2020-11-27Merge PR #13482: Improved error message on nested proofscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: gares Ack-by: jfehrle
2020-11-27[RM] script to notify "platform" projects to tagEnrico Tassi
2020-11-27Merge PR #13473: Testing {in _, _} and {pred _} from ssrboolcoqbot-app[bot]
Reviewed-by: gares
2020-11-27Improved error message on nested proofsFabian Kunze
to include most common reason when this happens on accident
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to ↵Pierre-Marie Pédrot
check resolution of evars more incrementally Ack-by: SkySkimmer Reviewed-by: gares Ack-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:34:03 +0000