Opened 11 years ago

Closed 9 years ago

#460 closed defect (worksforme)

proof general hanging on Coq Definition in file generated by Why3

Reported by: coquser Owned by: hendrik
Priority: major Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords:
Cc: alley.stoughton@…

Description

When I try to process the attached Coq file using ProofGeneral, it gets hung up on the Definition of IB6_IB7_QueryTags_First. In contrast, coqtop file works on this file. The file was generated by Why3's Coq driver, so maybe it's doing something that's syntactically unusual.

I'm running PG 4.1 on GNU Emacs 24.2.1. The Coq version is 8.3pl4.

Attachments (1)

easycrypt_IB6_IB7_QueryTags143e2c4.v​ (47.2 KB) - added by coquser 11 years ago.
problematic coq file

Download all attachments as: .zip

Change History (7)

Changed 11 years ago by coquser

Attachment: easycrypt_IB6_IB7_QueryTags143e2c4.v​ added

problematic coq file

comment:1 Changed 11 years ago by coquser

This may be a duplicate of #453, can you try setting proof-shell-process-connection-type to nil or upgrade to PG 4.2?

Bye,

Hendrik

comment:2 Changed 11 years ago by coquser

Owner: changed from David Aspinall to coquser
Status: new → assigned

comment:3 Changed 11 years ago by coquser

Owner: changed from coquser to hendrik

comment:4 Changed 11 years ago by coquser

I cannot reproduce this problem. Not even with PG 4.1, emacs 24.2.1 and Coq 8.3pl4. Do you still have this problem?

Hendrik

comment:5 Changed 9 years ago by coquser

Cannot reproduce it either in the latest CVS. --cpitcla

comment:6 Changed 9 years ago by courtieu

Resolution: → worksforme
Status: assigned → closed
Note: See TracTickets for help on using tickets.