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.

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

Adapt to coq/coq#19620 (Global.push_context_set no strict argument) #160

Merged
merged 2 commits into from
Oct 15, 2024

Conversation

SkySkimmer
Copy link
Contributor

No description provided.

@ppedrot
Copy link
Contributor

ppedrot commented Oct 14, 2024

Please merge now.

@ppedrot
Copy link
Contributor

ppedrot commented Oct 15, 2024

Ping @JasonGross

@SkySkimmer SkySkimmer marked this pull request as ready for review October 15, 2024 08:38
@JasonGross JasonGross enabled auto-merge (squash) October 15, 2024 09:07
@JasonGross
Copy link
Collaborator

This is not backwards compatible, it's failing with

File "src/Rewriter/Util/plugins/inductive_from_elim.ml", line 48, characters 10-12:
48 |       let () = Global.push_context_set ctx in
               ^^
Error: This pattern should not be a unit literal, the expected type is
       strict:bool -> unit

on the Alpine CI. Are you sure we should be changing the older versions of the code too?

@JasonGross JasonGross merged commit e4d987c into mit-plv:master Oct 15, 2024
8 checks passed
@SkySkimmer SkySkimmer deleted the push-context-strict branch October 15, 2024 10:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants