more formatting fixes

formatting fixes

minor cleanups, deleted dead code, eliminated use of (==) on CoreType

fix sortAlts so it actually does something

add tutorial.coqpass to gitignore

add tutorial to the repository

rename weakTypeToType'' to weakTypeToTypeOfKind

revise tyFunKind to use splitKind

add splitKind to HaskKind

fix ToString instance for Kind

minor cleanups in HaskStrongToWeak

include URL for trfrac.sty and mathpartir in LaTeX output

first pass at proper handling of coercions in HaskWeak

better error reporting in HaskWeakToStrong

better error reporting in Extraction.v

close numerous holes in HaskStrongToProof

major revision of HaskWeakToStrong, put phi/psi on the error monad

fix spelling error in HaskWeakToCore

remove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required

store the scrutinee CoreVar in WeakExpr Case to simplify WeakExprToCoreExpr

store the magic CoreVar for hetmet brak/esc in WeakExpr Esc/Brak

detect (->) TyCon and substitute FunTy in WeakToCore

fix bugs in LaTeX output

ToString instance for HaskCore

General.addErrorMessage, orErrorBindWithMessage

move eol:string to General.v

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