restore HaskWeakToStrong functionality that I broke over the weekend

Remove unnecessary coreVar_eq_refl axiom

Rename Extraction.fail to Extraction.Prelude_error

Eliminate the need for WeakVar decidable equality axiom

update push-url in Makefile

Make the HaskStrong type representation Kind-indexed, and many supporting changes (see long comment).

This patch makes a whole lot of interlocking changes, with the
ultimate (accomplished) goal of changing the HaskStrong type
representation ("HaskType") so that it is indexed by the Haskell Kind
of the type.  As a result, the auxiliary well-kindedness judgment
\vdash_{ty} is no longer necessary.

Other changes in this patch:

  - Added Coq ToString class (similar to Haskell's Show class)
  - Massive reduction in volume of code extracted for string literals
  - Decidable equality on HaskStrong's
  - Much more reliable HaskWeakToStrong, although it has regressed
    a bit in terms of number of cases handled; this will be remediated
    shortly.

more Makefile updates

Makefile updates

make latex output use the preview package to set the page size

add HaskProofToStrong skeleton implementation

add HaskStrongToWeak

add HaskStrongToProof

add HaskWeakToStrong

give HaskWeak its own type representation, fix numerous bugs

better names for the auxiliary CaseBranch records

separate type/coer/expr variables in HaskWeak case branches

store variables in ELetRecBindings rather than its indexing tree

add HaskWeakToCore

add proper proofs of the fact that every rule has exactly one conclusion

Changed WEBrak/WEEsc to store a CoreType

Added WeakVar, a separate variable representation for HaskWeak

added "publish" target to regenerate tex/pdf code

added HaskCoreToWeak

cleaned up lots of FIXMEs in ProofToLatex

Initial checkin of Coq-in-GHC code