Added dactuals to check-type-actuals and check-for-tccs* (type-name)
Made some term copies, in order to satisfy some asserts made in resolve and
set-type
Removed the use of current-declaration decl-formals in determining free-params
In gensubst* :around (expr), only do the type if not a name-expr, as that is
done in the resolution.
Minor reformatting
Fixed merge-subgoals to negate the ante conjunction when there are no succs
Modified expand-defn (lambda-expr) to generate a dependent type if needed
Modified get-typechecked-theory to make sure the call to get-theory is valid
1. Modified typecheck* (name) to prefer resolutions with dactuals over those
   without
2. Modified get-decl-resolutions to create a tynew with a better print-type
3. Refactored typecheck* (actual)
4. Modified compatible-uninstantiated? to make use of the existing actuals in
   creating bindings for find-compatible-bindings
1. Added dactuals to restore-object* :around (type-name)
2. Bound *bound-variables* in type-def-decl-saved-value
3. Added call to restore-object* for tval and dactuals in
   type-expr-from-print-type (type-name)
4. Added call to restore-object* for dactuals in
   type-expr-from-print-type (type-application)
1. Modified check-for-application-macro-tccs* to do nothing if bindings is nil,
   and to call make-projections correctly
2. Modified instantiable-operator-type to make the domain match the args
3. Significant reworking of instantiate-resolution and
   instantiate-operator-type, which used to try to handle one theory at a
   time in order to use subst-mod-params; now gets all bindings at once and
   calls subst-theory-params instead
4. Modified subst-for-formals? (modname) to check that theory associated with
   modname has formals
5. Added subst-for-formals? and subst-for-formals! (resolution) methods
Modified store-object to reset the *store-object-hash* if it is nil
1. Factored out subst-mod-params-print-type for setting the print-type from
   subst-mod-params* :around (t), and changed the way print-types are
   substituted.
2. Modified subst-mod-params* (name-expr) to ensure that the type is only
   substituted for once (in the resolution)
3. Modified subst-mod-params* (binding) to be more careful about the
   declared-type setting in the new substituted binding
Modified substit* (name-expr) to not substit in the type, but simply use the
type from the substituted resolution
Modified typecheck* (type-name) to only typecheck if there is no resolution
and no arguments
Minor changes
1. Modified find-compatible-bindings* to automatically include any
   decl-formals that may not appear in the bindings.
2. Modified set-tc-match-binding to match against the (cdr binding) if some
   decl-formal is in the bindings
3. Modified tc-match* (type-name) to call-next-method if earlier attempts fail
4. Modified tc-match-type-name-actuals to refine the final check
   before returning the initial bindings if all else fails
5. Misc fixes to tc-match-act
6. Added dactuals to tc-match* (name-expr name-expr)
1. Modified get-working-theory to use working_theory as is instead of
   working-theory
2. Modified add-working-decls to bind *typechecking-module*, *tccs*,
   *tccdecls*, *tccforms*, and(*exprs-generating-actual-tccs*
Modified lisp request to return a string
1. Fixed judgement-types* (lambda-expr) to generate dependent function types
   when necessary.
2. Minor fix to the nfield type in lift-recordtype-field-types*
3. Added type-predicates* (cotupletype)