coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Proofgeneral refuses to continue on warning
- Date: Wed, 20 Sep 2017 18:58:15 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=christoph.senjak AT ifi.lmu.de; spf=None smtp.mailfrom=christoph.senjak AT ifi.lmu.de; spf=None smtp.helo=postmaster AT acheron.ifi.lmu.de
- Ironport-phdr: 9a23:O4mOZxLFu83+8kXoutmcpTZWNBhigK39O0sv0rFitYgXLf/xwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBWB6kG1uDUVA1D0MRd/DuXzAI/bycqthM6o/JiGSAVShSGhZqtyaS63qALX/vIbh4lrKe5lwRvTo2BUfPxWg3hlI1CanD796Mb2+Jt+tShd7aFyv/VcWLn3KvxrBYdTCy4rZjg4
Hi.
I just upgraded to coq 8.7-beta, and now in proofgeneral I get warnings about not being able to define graphs of a function. Those warnings have been there in former versions, but emacs now refuses to continue, though it is just a warning. Does anyone know how to disable stopping at warnings, or what to do about this? My proofgeneral version is 4.4.
Best Regards
Christoph-Simon Senjak
- [Coq-Club] Proofgeneral refuses to continue on warning, Christoph-Simon Senjak, 09/20/2017
- Re: [Coq-Club] Proofgeneral refuses to continue on warning, Pierre Courtieu, 09/22/2017
Archive powered by MHonArc 2.6.18.