Skip to content

[Merged by Bors] - fix(Tactic/ExtractGoal): remove mathport's placeholder syntax for extract_goal#6707

Closed
joneugster wants to merge 4 commits intomasterfrom
eugster/mathport-syntax-extract_goal
Closed

[Merged by Bors] - fix(Tactic/ExtractGoal): remove mathport's placeholder syntax for extract_goal#6707
joneugster wants to merge 4 commits intomasterfrom
eugster/mathport-syntax-extract_goal

Conversation

@joneugster
Copy link
Copy Markdown
Contributor

@joneugster joneugster commented Aug 21, 2023 •
edited
Loading

extract_goal has been implemented in #4595.

Currently import Mathlib.Mathport.Syntax (or import Mathlib) overwrites this with a placeholder syntax yielding: tactic 'Mathlib.Tactic.extractGoal' has not been implemented

Open in Gitpod

@joneugster joneugster added awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. t-meta Tactics, attributes or user commands labels Aug 21, 2023
@joneugster joneugster changed the title fix: remove placeholder syntax for extract_goal fix(Tactic/ExtractGoal): remove mathport's placeholder syntax for extract_goal Aug 21, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 24, 2023
@kmill
Copy link
Copy Markdown
Contributor

kmill commented Aug 28, 2023

Thanks

bors r+

@bors
Copy link
Copy Markdown

bors bot commented Aug 28, 2023

👎 Rejected by label

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 28, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 28, 2023
@kmill
Copy link
Copy Markdown
Contributor

kmill commented Aug 28, 2023

bors r+

bors bot pushed a commit that referenced this pull request Aug 28, 2023
@joneugster @kmill
fix(Tactic/ExtractGoal): remove mathport's placeholder syntax for `ex…
bcd40be 
…tract_goal` (#6707)

`extract_goal` has been implemented in #4595. 

Currently `import Mathlib.Mathport.Syntax` (or `import Mathlib`) overwrites this with a placeholder syntax yielding: `tactic 'Mathlib.Tactic.extractGoal' has not been implemented`




Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Aug 28, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title fix(Tactic/ExtractGoal): remove mathport's placeholder syntax for extract_goal [Merged by Bors] - fix(Tactic/ExtractGoal): remove mathport's placeholder syntax for extract_goal Aug 28, 2023
@bors bors bot closed this Aug 28, 2023
@bors bors bot deleted the eugster/mathport-syntax-extract_goal branch August 28, 2023 15:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@joneugster @kmill