partial implementation of KappaAbs/KappaApp in Coq code
[coq-hetmet.git] / src / HaskStrong.v
2011-06-24 Adam Megaczallow quantification over any tyvar in the environment...
2011-05-31 Adam Megaczbetter error reporting in coreTypeToWeakType; dont...
2011-05-28 Adam Megaczmigrate HaskStrong away from using LeveledHaskType
2011-05-27 Adam Megaczrename variables to avoid Coq pickiness during extraction
2011-05-09 Adam Megaczsplit HaskLiteralsAndTyCons into two files
2011-05-09 Adam Megaczallow rank-1 polymorphic types for globals
2011-04-27 Adam Megaczprove all [admit]ted lemmas in HaskStrongToProof (not...
2011-03-29 Adam Megaczlots of cleanup
2011-03-25 Adam Megaczadd Concatenable, LatexMath, and fix HaskProofToLatex
2011-03-25 Adam Megaczadd ToLatex instance parameter to HaskStrong
2011-03-21 Adam Megaczmake StrongAlt a parameter rather than field in StrongC...
2011-03-20 Adam Megaczrequire all branches of LetRec be at the same level...
2011-03-19 Adam Megaczadd ToString instance for HaskStrong
2011-03-16 Adam Megaczadd EGlobal/RGlobal for CoreVars whose binder we cannot see
2011-03-15 Adam Megaczreshuffle definitions in an attempt to iron out inter...
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 Megaczstore variables in ELetRecBindings rather than its...
2011-03-02 Adam MegaczInitial checkin of Coq-in-GHC code