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

PVS Bug 512


Synopsis:        show-expanded-sequent does not show instanciations of inline operators
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Jan 12 13:00:02 2001
Originator:      Hendrik Tews
Organization:    inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  I noticed that in PVS 2.3 (in contrast to 2.2)
  show-expanded-sequent does neither show the theory nor the
  instanciations of inline operators. How can I access the
  instanciations?
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 
The actual problem is with infix operators - just test on any of them.
Fix: 
The fix is to pp* (infix-application), which should call-next-method if the operator has a mod-id, library, or actuals.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools