Modified match-modnames to handle dactuals
Added collect-pvs-file-decls-info to provide information supporting pvs
tooltips
Fixed some proofs
Added dactuals slot to various classes that were missing them
Minor change to str
1. Added a declare to fully-instantiated?
2. Modified free-params* (mapping) to handle free-params from the lhs
3. Fixed free-params-res which was not handling actuals and dactuals correctly
   when both were there.
Added pvs-add-tooltip command
Added id-place-list
1. Modified judgement-lt, judgement-subsumes, and add-judgement-decl to use
   simple-subtype-of? instead of subtype-of?
2. Modified get-lambda-expr-funtype-for-range* to correctly substitute for
   dependent types
3. Some optimizations to subtype-of-test
Modified mk-modname to create a declparam-modname when dactuals are provided.
Modified substit* (resolution) to substitute into the type even if the
modinst is eq after substitution
1. Added keyword-arg-symbol and update-prover-keywords
2. Added make-prover-keywords to include &key
Added source-formals and source-defn slots to defrule-entry
Modified create-compatible-modinsts to call mk-modname, which will ensure that
declparam-modname is created when needed
Fixed subst-mod-params-print-type (type-expr type-expr)
Modified subst-for-formals! (resolution) to create a declparam-modname if
dactuals are used.
Modified lemma-step to use forall-body* instead of expression when there are
no remaining-vars
1. Added declaration arg to calls to mk-modname when dacts are provided
2. Modified generate-adt-inline-map to set the associated-decls
1. Fixed tc-eq* (resolution resolution) to test tc-eq on dactuals, rather than
   allowing one or the other to be nil.
2. Fixed declaration-outside-formals? and actuals-are-outside-formals?
   to use the resolution
1. Modified check-arguments to call rule-rawname
2. Commented out the binding of * to '* in strat-eval*, which gets in the way
   of debugging this function
3. Lots of mods to pair-formal-args, etc. to allow for new &key arguments
4. Fixed let-form? to check for cons pair before taking the length (which
   breaks on conses)