B) break: repeated bindings in make-subtype-tcc-decl
A occurs whilst "tcp" is running proofs of proof obligations, but I've had it occur in proofs
done in previous versions of PVS that I have re-installed. It appears to be emitted by "grind".
It looks like some sort of lisp error. Doing the proofs again step by step gets rid of it altogether.
B is a total mystery to me: it occurs when type-checking. It is provoked by certain type declarations.
You can comment bits out to discover which declarations. These declarations look fine (e.g. they parse ok),
but they are always dependent-type declarations where certain fields are function types.
I re-jigged one declaration that was causing B and simplifying things mysteriously got rid of it.
But then when I declared a constant of said type, B returns when PVS type-checks that constant.
B worries me the most, since either a declaration is type-correct or it isn't. It can raise tccs but I don't see how no
tccs (provable or otherwise) can be defined for it.
thanks in advance