Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] ProofGeneral and ssreflect bullets

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] ProofGeneral and ssreflect bullets


Chronological Thread 
  • From: (Emilio Jesús Gallego Arias)
  • To: Florent Hivert <>
  • Cc: "ssreflect\@msr-inria.inria.fr" <>
  • Subject: Re: [ssreflect] ProofGeneral and ssreflect bullets
  • Date: Tue, 15 Mar 2016 00:48:12 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Neutral ; spf=None
  • Ironport-phdr: 9a23:3YA2bx26mDBscRYhsmDT+DRfVm0co7zxezQtwd8ZsegeKPad9pjvdHbS+e9qxAeQG96LtLQV1KGO7ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZXonLjss7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+mx3EVwaJ+jM8U3sbiAYAVybB6wv3WIu3kirku/Bh8C2APIv4V+Zndy6l6vJmYA+40GEALTFxsEzSi8hxi+p5rQkzvFRQyorQbY6SfNNkf6rGPIBJDVFdV9pcAnQSSri3aJECWq9YZb5V
  • Organization: X80 Heavy Industries
Florent Hivert
<>
writes:

> I got it. The culprits was the line
>
> '(coq-time-commands t)
>
> In my .gnu-emacs-custom
>
> Can someone confirm this behavior. If so, I'm filing a bug report to PG.

Good catch! Is not the first time (coq-time-commands) causes pain.

I can reproduce the bug now, it seems that PG tries to time the bullet:

<prompt>test < 20 |branch| 0 < </prompt>Time +

E.

Archive powered by MHonArc 2.6.18.

Top of Page