aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-03[refman] Fix error names.Théo Zimmermann
The @ syntax is not supported in the name, so we transform it manually as it would have been if no name had been provided.
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
2020-11-27Fix #13283: improved error on `clear implicit` flagFabian Kunze
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-27Merge PR #13491: Reactivate test-suite on MacOS X, accidently merged in #13476coqbot-app[bot]
Reviewed-by: gares
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
As discussed in the Coq meeting.
2020-11-26Reactivate test-suite on MacOS X, accidently merged in #13476.Hugo Herbelin
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26[environ] [typing_flags] Introduce helper function to remove duplicate codeEmilio Jesus Gallego Arias
2020-11-26[proofs] Support per-definition typing-flags in interactive proofs.Emilio Jesus Gallego Arias
Most cases should be accounted in proof code, however be wary of paths where `Global.env ()` is used.
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 16:19:48 +0000