clean up demo code
[coq-hetmet.git] / src / HaskProofToLatex.v
2011-05-31 Adam Megaczremove RLet and RWhere
2011-05-31 Adam Megaczlet RCut take a left environment as well
2011-05-31 Adam Megaczremove RJoin rule
2011-05-29 Adam Megaczadd RCut, RLeft, RRight rules
2011-05-28 Adam Megaczrename constructors of Arrange to start with A instead...
2011-05-28 Adam Megaczmove Arrange into NaturalDeductionContext
2011-05-27 Adam MegaczHaskProof: make the succedent level part of the judgment
2011-05-26 Adam Megaczadd new Where rule, eliminate unnecessary ga_swaps...
2011-05-15 Adam Megaczadd an identity production for Arrange
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 Megaczformatting fixes
2011-03-29 Adam Megaczlots of cleanup
2011-03-28 Adam Megaczreplace UJudg with Arrange
2011-03-25 Adam Megaczadd Concatenable, LatexMath, and fix HaskProofToLatex
2011-03-25 Adam Megaczadd ToLatex instance for TyCon/TyFun
2011-03-25 Adam MegaczHaskProofToLatex improvements
2011-03-25 Adam Megaczadd ToLatex class, move machinery to General.v
2011-03-20 Adam Megaczrequire all branches of LetRec be at the same level...
2011-03-16 Adam Megaczrestrict RNote to one hypothesis, major additions to...
2011-03-16 Adam Megaczadd EGlobal/RGlobal for CoreVars whose binder we cannot see
2011-03-15 Adam Megaczformatting
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-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 Megaczadd proper proofs of the fact that every rule has exact...
2011-03-07 Adam Megaczcleaned up lots of FIXMEs in ProofToLatex