Skip to content

Do not expose API relying on kernel instance substitution in EConstr. #18911

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
Merged
merged 2 commits into from
Apr 15, 2024
Merged

Do not expose API relying on kernel instance substitution in EConstr. #18911

merged 2 commits into from
Apr 15, 2024

Conversation

ppedrot
Copy link
Member

@ppedrot ppedrot commented Apr 8, 2024 •
edited
Loading

This defeats the purpose of EConstr.

Overlays:

@ppedrot ppedrot added kind: cleanup Code removal, deprecation, refactorings, etc. request: full CI Use this label when you want your next push to trigger a full CI. labels Apr 8, 2024
@ppedrot ppedrot added this to the 8.20+rc1 milestone Apr 8, 2024
@ppedrot ppedrot requested review from a team as code owners April 8, 2024 06:41
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 8, 2024
herbelin
herbelin approved these changes Apr 8, 2024
View reviewed changes
Copy link
Member

@herbelin herbelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK

ppedrot added a commit to ppedrot/Coq-Equations that referenced this pull request Apr 8, 2024
@ppedrot
Adapt w.r.t. rocq-prover/rocq#18911.
eae5546
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 8, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 8, 2024
@SkySkimmer SkySkimmer self-assigned this Apr 15, 2024
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 81784e9 into rocq-prover:master Apr 15, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Apr 15, 2024

@SkySkimmer: Please take care of the following overlays:

  • 18911-ppedrot-econstr-einstance-api.sh

@ppedrot ppedrot deleted the econstr-einstance-api branch April 15, 2024 14:05
ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Apr 15, 2024
@ppedrot
Merge pull request #588 from ppedrot/econstr-einstance-api
76b505f 
Adapt w.r.t. rocq-prover/rocq#18911.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@herbelin herbelin herbelin approved these changes

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@ppedrot @SkySkimmer @herbelin