aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-04Merge PR #13569: typocoqbot-app[bot]
Reviewed-by: jfehrle
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
Reviewed-by: kyoDralliam
2020-12-04Merge PR #13551: Stop calling Id.Map.domain on univ binders every individual ↵coqbot-app[bot]
universe Reviewed-by: herbelin
2020-12-04typoYves Bertot
2020-12-04Merge PR #13497: [rm] update release notescoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-04[rm] clarify process for is_a_released_version = trueEnrico Tassi
2020-12-04[rm] update git commands to push tagsEnrico Tassi
2020-12-04Merge PR #13527: Changes for Coq 8.13coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-12-03Merge PR #13546: [coqide] fix procedure to parse argumentscoqbot-app[bot]
Reviewed-by: ejgallego
2020-12-03Merge PR #13558: [refman] Fix error names.coqbot-app[bot]
Reviewed-by: jfehrle
2020-12-03Implement review corrections by Théo ZimmermannMatthieu Sozeau
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 #13548: Move *_with_full_binders variants out of the kernel.coqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-12-03[coqide] fix procedure to parse argumentsEnrico Tassi
coqide calls coqidetop -batch, if you are in -async-proof on then coqidetop spawns a worker and passes -batch to it. At some point, I could not find the commit, this made the worker die. On linux it seems it works anyway, but on windows this death is perceived by coqide which then does not start.
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-02Stop calling Id.Map.domain on univ binders every individual universeGaëtan Gilbert
2020-12-02Merge PR #13471: gitlab CI: remove redundant "dependencies" infocoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-02Move *_with_full_binders variants out of the kernel.Pierre-Marie Pédrot
They are not used there, and removing the redundance of the the case representation requires access to the environment, so we push their use further up.
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-30Adding a changelog for Ltac1.lambda.Pierre-Marie Pédrot
2020-11-30Add test for this new function.Pierre-Marie Pédrot
2020-11-30Add an abstraction function in the LtacX FFI.Pierre-Marie Pédrot
This allows to embed Ltac2 functions manipulating Ltac1 values as simple Ltac1 values.
2020-11-30Store Ltac2 valexpr instead of unevaluated code inside Ltac1 value embedding.Pierre-Marie Pédrot
This should have the same semantics, it is just a matter of moving the responsibility of evaluating the thunk from the Ltac1 application tactic to the quotation.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:49:51 +0000