update baked in CoqPass.hs
[coq-hetmet.git] / src / HaskStrongTypes.v
2011-05-27 Adam MegaczHaskProof: make the succedent level part of the judgment
2011-05-27 Adam Megaczrename variables to avoid Coq pickiness during extraction
2011-05-14 Adam Megaczintegrate skolemization pass with flattening
2011-05-12 Adam Megaczrewrite {take,drop}_arg_types to avoid use of equality...
2011-05-12 Adam MegaczHaskStrongTypes: add {take,drop}_arg_types
2011-05-09 Adam Megaczsplit HaskLiteralsAndTyCons into two files
2011-05-09 Adam Megaczabstract out the kind of environment classifiers (ECKind)
2011-05-09 Adam Megaczallow rank-1 polymorphic types for globals
2011-03-29 Adam Megaczlots of cleanup
2011-03-25 Adam Megaczadd Concatenable, LatexMath, and fix HaskProofToLatex
2011-03-25 Adam Megaczremove unnecessary instance from HaskStrongTypes
2011-03-20 Adam Megaczrequire all branches of LetRec be at the same level...
2011-03-15 Adam Megaczfinal batch of fixups before enabling -fcoqpass
2011-03-15 Adam Megaczchange names of Kind constructors to be more informative
2011-03-15 Adam Megaczreshuffle definitions in an attempt to iron out inter...
2011-03-14 Adam Megaczfirst pass at proper handling of coercions in HaskWeak
2011-03-14 Adam Megaczfix bugs in LaTeX output
2011-03-13 Adam Megaczrestore HaskWeakToStrong functionality that I broke...
2011-03-12 Adam MegaczMake the HaskStrong type representation Kind-indexed...
2011-03-07 Adam Megaczgive HaskWeak its own type representation, fix numerous...
2011-03-07 Adam Megaczbetter names for the auxiliary CaseBranch records
2011-03-07 Adam MegaczAdded WeakVar, a separate variable representation for...
2011-03-02 Adam MegaczInitial checkin of Coq-in-GHC code