Skip to content

[coqide] Fix code to display goal in both top script and current script buffers #15912

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
May 14, 2022
Merged

[coqide] Fix code to display goal in both top script and current script buffers #15912

merged 1 commit into from
May 14, 2022

Conversation

jfehrle
Copy link
Member

@jfehrle jfehrle commented Apr 6, 2022

Fixes: #15903

Attn: @MSoegtropIMC

@jfehrle jfehrle added kind: fix This fixes a bug or incorrect documentation. part: ltac debugger Issues and PRs related to the Ltac debugger, visual CoqIDE debugger etc. labels Apr 6, 2022
@jfehrle jfehrle added this to the 8.15.2 milestone Apr 6, 2022
@jfehrle jfehrle requested a review from a team as a code owner April 6, 2022 21:14
@jfehrle jfehrle mentioned this pull request Apr 8, 2022
Closed
@proux01 proux01 changed the title Fix code to display goal in both top script and current script buffers [coqide] Fix code to display goal in both top script and current script buffers Apr 12, 2022
@ppedrot
Copy link
Member

ppedrot commented May 9, 2022

Any tester before I merge?

@ppedrot ppedrot self-assigned this May 9, 2022
@ppedrot
Copy link
Member

ppedrot commented May 14, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 7a0c611 into rocq-prover:master May 14, 2022
SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request May 25, 2022
@SkySkimmer
Backport PR rocq-prover#15912: [coqide] Fix code to display goal in b…
7889f1f 
…oth top script and current script buffers
SkySkimmer added a commit to SkySkimmer/rocq that referenced this pull request May 25, 2022
@SkySkimmer
Backport PR rocq-prover#15912: [coqide] Fix code to display goal in b…
53d35db 
…oth top script and current script buffers
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation. part: ltac debugger Issues and PRs related to the Ltac debugger, visual CoqIDE debugger etc.
Projects
None yet
Milestone
8.15.2
Development

Successfully merging this pull request may close these issues.

Ltac Debugger: goals not updated when one steps through tactics defined in different files.
2 participants
@jfehrle @ppedrot