How to get coq to print out new goal and hypotheses after applying tactic












1














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







share|improve this question
























  • 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
















1














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







share|improve this question
























  • 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














1












1








1







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







share|improve this question















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






share|improve this question















share|improve this question













share|improve this question




share|improve this question








edited Nov 13 '18 at 22:05







user2423780

















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


















  • 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












1 Answer
1






active

oldest

votes


















1














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.






share|improve this answer





















    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
    });


    }
    });














    draft saved

    draft discarded


















    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









    1














    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.






    share|improve this answer


























      1














      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.






      share|improve this answer
























        1












        1








        1






        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.






        share|improve this answer












        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.







        share|improve this answer












        share|improve this answer



        share|improve this answer










        answered Nov 14 '18 at 14:53









        Tej ChajedTej Chajed

        2,750715




        2,750715






























            draft saved

            draft discarded




















































            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.





            Some of your past answers have not been well-received, and you're in danger of being blocked from answering.


            Please pay close attention to the following guidance:


            • 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.




            draft saved


            draft discarded














            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





















































            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







            -

            這個網誌中的熱門文章

            Xamarin.form Move up view when keyboard appear

            圖片
            .everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ height:90px;width:728px;box-sizing:border-box; } 0 I'm trying to build a Chat app UI, the idea of the Layout was pretty simple: When the input bar is focused, keyboard show up and "push" up the chat bar, as it's a grid, the ListView will resize to fit the screen: I update the input bar's margin to "push" it up: NSValue result = (NSValue)args.Notification.UserInfo.ObjectForKey(new NSString(UIKeyboard.FrameEndUserInfoKey)); CGSize keyboardSize = result.RectangleFValue.Size; if (Element != null){ Element.Margin = new Thickness(0, 0, 0,keyboardSize.Height); //push the entry up to keyboard height when keyboard is activated } And this is ...
            閱讀完整內容

            Post-Redirect-Get with Spring WebFlux and Thymeleaf

            圖片
            .everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ height:90px;width:728px;box-sizing:border-box; } 2 Can someone explain to me how to implement the post-redirect-get pattern in Spring WebFlux and Thymeleaf? What subscribes on the database save method? @GetMapping("/register") public String showRegisterForm(Model model) { model.addAttribute("user", new User()); return "register"; } @PostMapping public String processRegisterForm(@Valid User user, BindingResult bindingResult) { if (bindingResult.hasErrors()) { return "register"; } else { userRepository.save(user); //what subscribes on this? //how to redirect on e.g. "/login"? ...
            閱讀完整內容

            Anylogic : not able to use stopDelay()

            圖片
            -2 I am building a railway station model. I want a train to depart when I click a button. I want to call stopDelay() for that but I am not sure how to do that and from which place. anylogic share | improve this question asked Nov 23 '18 at 10:12 Anupam Singh Anupam Singh 1 Hi Anupam, welcome to SOF. Please check how to ask good questions, see link below. Your question is...
            閱讀完整內容