split Extraction.v so most can be compiled with -dont-load-proofs
add HaskXXXXCategory, generalized arrows, and reifications
make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch
require all branches of LetRec be at the same level in HaskProof
improve HaskProofToStrong, although its messier now
major overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial
reshuffle definitions in an attempt to iron out inter-file dependenceies
rename weakTypeToType'' to weakTypeToTypeOfKind
include URL for trfrac.sty and mathpartir in LaTeX output
better error reporting in Extraction.v
major revision of HaskWeakToStrong, put phi/psi on the error monad
restore HaskWeakToStrong functionality that I broke over the weekend
Rename Extraction.fail to Extraction.Prelude_error
Eliminate the need for WeakVar decidable equality axiom
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.
make latex output use the preview package to set the page size
add HaskProofToStrong skeleton implementation
add HaskStrongToWeak
add HaskStrongToProof
Changed WEBrak/WEEsc to store a CoreType