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

Fixing bugs introduced in change_no_check #10059

Merged
merged 2 commits into from May 5, 2019

Conversation

Projects
None yet
3 participants
@herbelin
Copy link
Member

commented May 3, 2019

Kind: bug fix

This fixes a bug of #10017 reported in #10053 which was introduced while merging the initial version of #10017 with #9983. This also adds an item in CHANGES.

  • Added / updated test-suite

  • Entry added in CHANGES.md.

herbelin added some commits Apr 30, 2019

Tactics: fixing "change_no_check in".
(Merge of the initial version with #9983 was broken)

@herbelin herbelin requested a review from ppedrot as a code owner May 3, 2019

@Zimmi48 Zimmi48 added the kind: fix label May 4, 2019

@Zimmi48 Zimmi48 added this to the 8.11+beta1 milestone May 4, 2019

@ppedrot ppedrot self-assigned this May 4, 2019

@ppedrot

ppedrot approved these changes May 4, 2019

Copy link
Member

left a comment

The first part would have been fixed by #10052 if I'm not mistaken, but let's fix it right now.

@ppedrot

This comment has been minimized.

Copy link
Member

commented May 4, 2019

Are the CI failures related?

@ppedrot ppedrot merged commit a0cfcc3 into coq:master May 5, 2019

9 checks passed

GitLab CI pipeline Pipeline completed on GitLab CI
Details
coq.coq Build #20190503.25 succeeded
Details
coq.coq (Windows) Windows succeeded
Details
coq.coq (macOS) macOS succeeded
Details
doc:ml-api:odoc: ml-api artifact Link to ml-api build artifact.
Details
doc:refman: refman artifact Link to refman build artifact.
Details
doc:refman: stdlib artifact Link to stdlib build artifact.
Details
library:ci-fiat-crypto-legacy Test succeeded on GitLab CI after being retried
Details
pkg:nix Test succeeded on GitLab CI after being retried
Details

ppedrot added a commit that referenced this pull request May 5, 2019

@Zimmi48 Zimmi48 referenced this pull request May 5, 2019

Merged

Unreleased changelog folder #9964

4 of 5 tasks complete

vbgl added a commit to vbgl/coq that referenced this pull request May 6, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.