[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Latex in pvs

Hi, I'm having trouble running latex on my theories.  I get the

The slot name is missing from the object
#<auto-rewrite-plus-decl sq_simrel.nil> of class
#<standard-class auto-rewrite-plus-decl> during operation slot-value

when running M-x latex-{theory,pvs-file}.  However there seems to be
no trouble generating latex for proofs (M-x latex-proof).

It looks like bugs 770, 812 and 823 are relevant, but I can't seem
to get any useful info from the bug reports.  Any help appreciated