How to get coq to print out new goal and hypotheses after applying tactic
sometimes I find coq gets into a state where when I apply a tactic, the new goal and hypotheses don't automatically get printed out. How do I set it to print these out after each tactic invocation.
This is coq 8.7.2, using coqtop
coq
asked Nov 13 '18 at 3:04
user2423780user2423780
283
add a comment |
sometimes I find coq gets into a state where when I apply a tactic, the new goal and hypotheses don't automatically get printed out. How do I set it to print these out after each tactic invocation.
This is coq 8.7.2, using coqtop
coq
asked Nov 13 '18 at 3:04
user2423780user2423780
283
What is your Coq version? What user interface are you using?
– ejgallego
Nov 13 '18 at 10:59
I'm not OP but I've seen this happen with Proof General, but I haven't investigated why. In the meantime, you can use C-c C-p to refresh the goal window.
– Li-yao Xia
Nov 13 '18 at 15:54
I believe this is more a problem with older versions of ProofGeneral than with newer ones
– Jason Gross
Nov 13 '18 at 16:54
1
I opened an issue with a minimized example github.com/ProofGeneral/PG/issues/403
– Li-yao Xia
Nov 14 '18 at 16:16
add a comment |
sometimes I find coq gets into a state where when I apply a tactic, the new goal and hypotheses don't automatically get printed out. How do I set it to print these out after each tactic invocation.
This is coq 8.7.2, using coqtop
coq
asked Nov 13 '18 at 3:04
user2423780user2423780
283
sometimes I find coq gets into a state where when I apply a tactic, the new goal and hypotheses don't automatically get printed out. How do I set it to print these out after each tactic invocation.
This is coq 8.7.2, using coqtop
coq
coq
asked Nov 13 '18 at 3:04
user2423780user2423780
283
asked Nov 13 '18 at 3:04
user2423780user2423780
283
edited Nov 13 '18 at 22:05
user2423780
asked Nov 13 '18 at 3:04
user2423780user2423780
283
asked Nov 13 '18 at 3:04
user2423780user2423780
283
asked Nov 13 '18 at 3:04
user2423780user2423780
283
283
What is your Coq version? What user interface are you using?
– ejgallego
Nov 13 '18 at 10:59
I'm not OP but I've seen this happen with Proof General, but I haven't investigated why. In the meantime, you can use C-c C-p to refresh the goal window.
– Li-yao Xia
Nov 13 '18 at 15:54
I believe this is more a problem with older versions of ProofGeneral than with newer ones
– Jason Gross
Nov 13 '18 at 16:54
1
I opened an issue with a minimized example github.com/ProofGeneral/PG/issues/403
– Li-yao Xia
Nov 14 '18 at 16:16
add a comment |
What is your Coq version? What user interface are you using?
– ejgallego
Nov 13 '18 at 10:59
I'm not OP but I've seen this happen with Proof General, but I haven't investigated why. In the meantime, you can use C-c C-p to refresh the goal window.
– Li-yao Xia
Nov 13 '18 at 15:54
I believe this is more a problem with older versions of ProofGeneral than with newer ones
– Jason Gross
Nov 13 '18 at 16:54
1
I opened an issue with a minimized example github.com/ProofGeneral/PG/issues/403
– Li-yao Xia
Nov 14 '18 at 16:16
What is your Coq version? What user interface are you using?
– ejgallego
Nov 13 '18 at 10:59
What is your Coq version? What user interface are you using?
– ejgallego
Nov 13 '18 at 10:59
I'm not OP but I've seen this happen with Proof General, but I haven't investigated why. In the meantime, you can use C-c C-p to refresh the goal window.
– Li-yao Xia
Nov 13 '18 at 15:54
I'm not OP but I've seen this happen with Proof General, but I haven't investigated why. In the meantime, you can use C-c C-p to refresh the goal window.
– Li-yao Xia
Nov 13 '18 at 15:54
I believe this is more a problem with older versions of ProofGeneral than with newer ones
– Jason Gross
Nov 13 '18 at 16:54
I believe this is more a problem with older versions of ProofGeneral than with newer ones
– Jason Gross
Nov 13 '18 at 16:54
1
1
I opened an issue with a minimized example github.com/ProofGeneral/PG/issues/403
– Li-yao Xia
Nov 14 '18 at 16:16
I opened an issue with a minimized example github.com/ProofGeneral/PG/issues/403
– Li-yao Xia
Nov 14 '18 at 16:16
add a comment |
1 Answer
1
active
oldest
votes
I believe when this happens it's a bug in Proof General, which is supposed to display the proof context whenever you're in the middle of a proof. Li-yao Xia's solution of hitting C-c C-p should work.
answered Nov 14 '18 at 14:53
Tej ChajedTej Chajed
2,750715
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53273184%2fhow-to-get-coq-to-print-out-new-goal-and-hypotheses-after-applying-tactic%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
I believe when this happens it's a bug in Proof General, which is supposed to display the proof context whenever you're in the middle of a proof. Li-yao Xia's solution of hitting C-c C-p should work.
answered Nov 14 '18 at 14:53
Tej ChajedTej Chajed
2,750715
add a comment |
I believe when this happens it's a bug in Proof General, which is supposed to display the proof context whenever you're in the middle of a proof. Li-yao Xia's solution of hitting C-c C-p should work.
answered Nov 14 '18 at 14:53
Tej ChajedTej Chajed
2,750715
add a comment |
I believe when this happens it's a bug in Proof General, which is supposed to display the proof context whenever you're in the middle of a proof. Li-yao Xia's solution of hitting C-c C-p should work.
answered Nov 14 '18 at 14:53
Tej ChajedTej Chajed
2,750715
I believe when this happens it's a bug in Proof General, which is supposed to display the proof context whenever you're in the middle of a proof. Li-yao Xia's solution of hitting C-c C-p should work.
answered Nov 14 '18 at 14:53
Tej ChajedTej Chajed
2,750715
answered Nov 14 '18 at 14:53
Tej ChajedTej Chajed
2,750715
answered Nov 14 '18 at 14:53
Tej ChajedTej Chajed
2,750715
answered Nov 14 '18 at 14:53
Tej ChajedTej Chajed
2,750715
2,750715
add a comment |
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53273184%2fhow-to-get-coq-to-print-out-new-goal-and-hypotheses-after-applying-tactic%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
What is your Coq version? What user interface are you using?
– ejgallego
Nov 13 '18 at 10:59
I'm not OP but I've seen this happen with Proof General, but I haven't investigated why. In the meantime, you can use C-c C-p to refresh the goal window.
– Li-yao Xia
Nov 13 '18 at 15:54
I believe this is more a problem with older versions of ProofGeneral than with newer ones
– Jason Gross
Nov 13 '18 at 16:54
1
I opened an issue with a minimized example github.com/ProofGeneral/PG/issues/403
– Li-yao Xia
Nov 14 '18 at 16:16