Added save-some-pvs-buffers to show-tccs
Fixed step-proof to not go to *pvs* buffer if there is an error
Modified resolution-string to include dactuals
Added :pvs to intern
Fixed exports and added package names to calls to intern
Modified INSTALL to reference Git rather than SVN
1. Modified resolve-with-actuals to be more careful about checking the length
   of actuals (dactuals may be involved)
2. Modified compatible-uninstantiated? (t) to only use the formals of a theory
   if it is not the current-theory
Fixed type-expr-from-print-type (type-application) to not use
with-declaration, and instead to subst-mod-params if there are dactuals in the
theory instance.
Modified set-type* :around (application) to add nil to the call to beta-reduce
in the application case - this was requested by Cesar
Fixed set-tc-match-binding to take account of dep-bindings
Fixed get-current-imported-theories to not call libref-to-libid - a libid is
not always available, and get-theory* works better with a lib-ref anyway,
Misc
Added to the export list
Added current-context-path and modified exports
Added *pvs-warning-hooks* and some exports
Added to export
Added to export
Modified typecheck-file to give an error if the file is not found
Added to export
Modified set-type* :around (cases-expr) to check that call-next-method returns
a cases-expr (conversions may have been added).