Skip to content

[Merged by Bors] - fix: fun.: construct correct matchDiscr syntax#273

Closed
gebner wants to merge 3 commits intomasterfrom
nomatchstx
Closed

[Merged by Bors] - fix: fun.: construct correct matchDiscr syntax#273
gebner wants to merge 3 commits intomasterfrom
nomatchstx

Conversation

@gebner
Copy link
Copy Markdown
Member

@gebner gebner commented May 22, 2022

Fixes #272

@gebner
Copy link
Copy Markdown
Member Author

gebner commented May 22, 2022

bors r+

bors bot pushed a commit that referenced this pull request May 22, 2022
@bors
Copy link
Copy Markdown

bors bot commented May 22, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix: fun.: construct correct matchDiscr syntax [Merged by Bors] - fix: fun.: construct correct matchDiscr syntax May 22, 2022
@bors bors bot closed this May 22, 2022
@bors bors bot deleted the nomatchstx branch May 22, 2022 12:00
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.

nomatch tactic introduces sorryAx

1 participant