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.
Note: See
TracTickets for help on using
tickets.
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.