Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proofgeneral refuses to continue on warning

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proofgeneral refuses to continue on warning


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Proofgeneral refuses to continue on warning
  • Date: Fri, 22 Sep 2017 17:00:57 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f182.google.com
  • Ironport-phdr: 9a23:28wrQhZM5q2Ssxz7GLqiUs7/LSx+4OfEezUN459isYplN5qZpsq+bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76vnYuHUD0MhMwLeDoEKbTid623qa84c79eQJN0QK8bKloIV2dqhjLqsgbnMM2Mqc80AHE5HBPZv5KxG51DV2Wlhf4oMy3+cgwoGxrp/s9+psYAu3BdKMiQOkAAQ==

Hi
You should switch to a more recent version. 

The best is to clone the github repository of Proofgeneral.

If your problems are still there please consider submitting a bug in pg's github page. 

Best regards
P

Le mer. 20 sept. 2017 à 18:58, Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de> a écrit :
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



Archive powered by MHonArc 2.6.18.

Top of Page