Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 675


Synopsis:        typo in System Guide
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Jun 12 11:15:00 2002
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  there is an unfortunate typo on page 56 in the system guide: 
  status-proof is bound to C-c C-s p. 
  
  Typing C-c s p does install-proof which (very likely) overwrites
  the currently installed proof. 
  
  For less experienced users it would probably be nice to explain
  in Section 3.5.4 how to recover an overwritten proof from a
  (wrong) install-proof.
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 
Modified install-and-step-proof to ask before installing the proof, and
checked that the user guide includes how to get the old proof back (using
display-proof-formula).
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools