remove all admits from ProgrammingLanguage.v
[coq-hetmet.git] / src / HaskProofToStrong.v
2011-04-10 Adam Megaczupdate to new coq-categories, base ND_Relation on inert...
2011-03-29 Adam Megaczformatting fixes
2011-03-29 Adam Megaczswap the order of the hypotheses of RLet
2011-03-28 Adam Megaczreplace UJudg with Arrange
2011-03-25 Adam Megaczadd Concatenable, LatexMath, and fix HaskProofToLatex
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 Megaczcheckpoint
2011-03-19 Adam Megaczimprove HaskProofToStrong, although its messier now
2011-03-16 Adam Megaczrestrict RNote to one hypothesis, major additions to...
2011-03-12 Adam MegaczMake the HaskStrong type representation Kind-indexed...
2011-03-07 Adam Megaczadd HaskProofToStrong skeleton implementation