Opened 13 years ago

Closed 13 years ago

#414 closed defect (fixed)

PG thinks Preterm command is not state-preserving

Reported by: Robin Green Owned by: David Aspinall
Priority: trivial Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc:

Description

Preterm is not listed in the Coq commands database, so PG incorrectly(?) thinks it is not state-preserving and refuses to execute it from C-c C-v.

Change History (1)

comment:1 Changed 13 years ago by courtieu

Resolution: fixed
Status: newclosed

Fixed in cvs. Thank you for submitting. Also added "Obligations" in state-preserving commands. Sadly there is currently no way of keeping track of all state preserving commands, except by hand like this. You can still set the "strict state preserving" customization variable to nil.

Note: See TracTickets for help on using tickets.