Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Next master #565

Merged
merged 48 commits into from
Dec 29, 2023
Merged

Next master #565

merged 48 commits into from
Dec 29, 2023

Conversation

gares
Copy link
Contributor

@gares gares commented Dec 23, 2023

No description provided.

proux01 and others added 30 commits July 7, 2023 15:01
@proux01
Adapt to coq/coq#17823
b21d4a3
@gares
Merge pull request #479 from proux01/coq_17823
38d0528 
Adapt to coq/coq#17823
@SkySkimmer
Adapt to coq/coq#17818 (APIs moved to Vernactypes)
a9eb74d
@proux01
Adapt to coq/coq#17827
2d4c43a
@gares
Merge pull request #490 from proux01/coq_17827
0ab62d5 
Adapt to Coq #17827
@ppedrot
Adapt w.r.t. coq/coq#17955.
5c23e96
@proux01
Merge remote-tracking branch 'origin/master' into coq-master
fbb68b1
@gares
Merge pull request #498 from proux01/coq-master_merge
a0d0eef 
Merge master into coq-master
@SkySkimmer
Merge pull request #494 from ppedrot/hint-cut-static-globref
2aeae2e
@SkySkimmer
Adapt to coq/coq#17795 (ComInductive API and glob_sort changes)
4a1c8ae
@ppedrot
Merge pull request #474 from SkySkimmer/comind-level-compute
a713f87 
Adapt to coq/coq#17795 (ComInductive API uses econstr more)
@SkySkimmer
Adapt to coq/coq#17667 (Genintern.register_subst0 moved to Gensubst)
b8e9df2
Adapt to coq/coq#18023 (RedFlags moving out of CClosure)
d010b5a
@SkySkimmer
Merge pull request #481 from SkySkimmer/vernactypes
b1f7d4a
@SkySkimmer
Merge pull request #502 from rlepigre/br/cleanup-cclosure
bc38f3f
@SkySkimmer
Automatic change in elpi-builtin
f0ca80b 
Every time I run ci-elpi_hb from coq upstream this change wants to
happen
@gares
Merge pull request #504 from SkySkimmer/elpi-builtin
6f5614b 
Automatic change in elpi-builtin
@SkySkimmer
Adapt to coq/coq#17836 (sort poly)
6b90934
@herbelin
Adapt to Coq PR #18007: Proof_using.definition_using takes names of r…
040cd23 
…ecursive definitions as extra arguments.
@ppedrot
Merge pull request #513 from herbelin/coq-master+adapt-coq-pr18007-ex…
f494235 
…tra-checks-proof-using

Adapt to Coq PR #18007: Proof_using.definition_using takes names of fixpoints being built
@SkySkimmer
Adapt to coq/coq#18187 (reductionbehaviour is on constant not gref)
fdcce15
@ppedrot
Merge pull request #526 from SkySkimmer/redbehaviour-pred
7075a45 
 Adapt to coq/coq#18187 (reductionbehaviour is on constant not gref)
@herbelin
Removing superfluous poly flag for try_add_new_coercion and declare_a…
9bb2338 
…xiom.
@SkySkimmer
Merge pull request #503 from SkySkimmer/sort-poly
fca6a37
@ppedrot
Adapt w.r.t. coq/coq#17136.
1a81969
@ppedrot
Merge pull request #534 from ppedrot/stream_error_to_gramlib
f0b4b9c 
Adapt w.r.t. coq/coq#17136.
@SkySkimmer
Adapt to coq/coq#18280 (case relevance outside case info)
bb9c54d
@ppedrot
Adapt w.r.t. coq/coq#18294.
9ad9c44
@SkySkimmer
Merge pull request #542 from ppedrot/glob-evar-kinds
4b050c6
@SkySkimmer
Merge pull request #541 from SkySkimmer/ci-relevance
f6bed81
ppedrot and others added 15 commits November 15, 2023 12:02
@ppedrot
Merge pull request #500 from SkySkimmer/pattern-quotations
4587e02 
Adapt to coq/coq#17667 (Genintern.register_subst0 moved to Gensubst)
@ppedrot
Adapt w.r.t. coq/coq#18312.
71a82a5
@herbelin
This is to adapt to coq/coq#8190.
3c08a3c 
Function cbv_norm_flags now needs to know if the reduction is expected
to be weak or strong. We set it to strong:true preserving the previous
semantics.
@SkySkimmer
Merge pull request #547 from ppedrot/detuplify-impargs
4a1a6d9
@SkySkimmer
Adapt to coq/coq#18331 (mind_kelim -> mind_squashed)
131853c
@SkySkimmer
Merge pull request #528 from herbelin/coq-master+adapt-coq-pr18190-wh…
9e23b0f 
…d-cbv
@ppedrot
Adapt w.r.t. coq/coq#18345.
41c5fd3
@ppedrot
Merge pull request #533 from herbelin/coq-master+adapt-coq-pr18253-no…
b8752c6 
…-poly-for-coercion

Adapt to Coq PR #18253: poly flag is spurious on try_add_new_coercion
@ppedrot
Merge pull request #548 from SkySkimmer/sort-poly-ind
d85ca2d 
Adapt to coq/coq#18331 (mind_kelim -> mind_squashed)
@SkySkimmer
Merge pull request #550 from ppedrot/harden-vernacextend-naming
b753aa4
@gares
Merge branch 'coq-master'
d17285e
@gares
master on 8.19
0ef2f9b
@gares
nix
b525f72
@gares
import classes from 8.19
e8f64e8
@gares
nix
feb3c84
@gares
Copy link
Contributor Author

gares commented Dec 23, 2023

@CohenCyril do you know why the nix job picks up an old version of coq-elpi and not this branch?

@gares
Copy link
Contributor Author

gares commented Dec 24, 2023

Thanks @CohenCyril I now see it passes MC and OOthm, so I'm OK releasing this branch.
But there is a problem with finmap, otherwise I'd love to also test MCA before releasing.

@gares gares merged commit a8bcaf1 into master Dec 29, 2023
49 of 55 checks passed
@gares gares deleted the next-master branch December 29, 2023 14:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@gares @CohenCyril @proux01 @SkySkimmer @ppedrot @herbelin