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

[coq] Adapt to coq/coq#6454 "forbid calling to_constr on open terms" #55

Merged
merged 1 commit into from
Apr 13, 2018

Conversation

ejgallego
Copy link
Contributor

@ejgallego ejgallego commented Feb 14, 2018

This PR is IMO interesting and seems to suggest quite a few Coq API modifications that are a must.

In particular coq/coq#6310 seems like one of the most flagrant omissions from the EConstr API.

@ejgallego ejgallego force-pushed the evar+strict_to_constr branch from 2f6e057 to 9372934 Compare February 14, 2018 17:12
@ejgallego ejgallego force-pushed the evar+strict_to_constr branch from 9372934 to 054f105 Compare March 1, 2018 00:43
@ejgallego ejgallego force-pushed the evar+strict_to_constr branch from 054f105 to a9fe0af Compare March 31, 2018 04:04
This PR is IMO interesting and seems to suggest quite a few Coq API
modifications that are a must.

In particular coq/coq#6310 seems like one of the most flagrant omissions from
the EConstr API. Some other issues found are with `Inductives`,
`Obligations` and missing functions from `Term`.
@ejgallego ejgallego force-pushed the evar+strict_to_constr branch from a9fe0af to 75fbad3 Compare March 31, 2018 16:33
@ppedrot
Copy link
Collaborator

ppedrot commented Apr 13, 2018

The PR has made it into Coq. Can you merge this one?

@mattam82 mattam82 merged commit a4b1c12 into mattam82:8.8+alpha Apr 13, 2018
@mattam82
Copy link
Owner

Done, thanks!

@ejgallego ejgallego deleted the evar+strict_to_constr branch April 13, 2018 11:25
@maximedenes
Copy link
Contributor

This was merged to the wrong branch and breaks Coq's 8.8 CI. Please fix ASAP, given how close we are to the release.

@Zimmi48
Copy link
Contributor

Zimmi48 commented Apr 13, 2018

Shit @mattam82, didn't you see what I wrote in coq/coq#7205? Your 8.8+alpha branch is now incompatible with Coq 8.8 and consequently our CI for v8.8 is going to be broken.

@Zimmi48
Copy link
Contributor

Zimmi48 commented Apr 13, 2018

FTR the solution is to create a new branch 8.9+alpha from this branch, and to revert this PR in 8.8+alpha only.

@ejgallego
Copy link
Contributor Author

In some version of the CI documents, a standard branch naming for CI contribs was suggested, maybe it is time we start to enforce it and thus submit issues to all devs upstream. However, this may be a delicate issue.

@Zimmi48
Copy link
Contributor

Zimmi48 commented Apr 13, 2018

I think that the naming scheme is not the problem here.

@ejgallego
Copy link
Contributor Author

Indeed, sorry for the mistake, let me rephrase my statement "a standard branch layout for CI contribs was suggested".

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.

None yet

5 participants