projects / coq-hetmet.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
merge proof correction
[coq-hetmet.git] / src / HaskStrongToProof.v
2011-06-24 Adam Megaczallow quantification over any tyvar in the environment... commit | commitdiff
2011-06-21 Adam Megaczadd crude support for flattening with LetRec and Case... commit | commitdiff
2011-06-02 Adam Megaczadd support for flattening recursive-let commit | commitdiff
2011-05-31 Adam Megaczremove RLet and RWhere commit | commitdiff
2011-05-31 Adam Megaczlet RCut take a left environment as well commit | commitdiff
2011-05-31 Adam Megaczremove RJoin rule commit | commitdiff
2011-05-28 Adam Megaczrename constructors of Arrange to start with A instead... commit | commitdiff
2011-05-28 Adam Megaczmove Arrange into NaturalDeductionContext commit | commitdiff
2011-05-28 Adam Megaczmigrate HaskStrong away from using LeveledHaskType commit | commitdiff
2011-05-27 Adam MegaczHaskProof: make the succedent level part of the judgment commit | commitdiff
2011-05-27 Adam Megaczrename variables to avoid Coq pickiness during extraction commit | commitdiff
2011-05-26 Adam Megaczadd new Where rule, eliminate unnecessary ga_swaps... commit | commitdiff
2011-05-12 Adam Megaczswap order of hypotheses in RApp to match RLet commit | commitdiff
2011-05-09 Adam Megaczallow rank-1 polymorphic types for globals commit | commitdiff
2011-04-27 Adam Megaczprove all [admit]ted lemmas in HaskStrongToProof (not... commit | commitdiff
2011-03-29 Adam Megaczformatting fixes commit | commitdiff
2011-03-29 Adam Megaczlots of cleanup commit | commitdiff
2011-03-29 Adam Megaczswap the order of the hypotheses of RLet commit | commitdiff
2011-03-28 Adam Megaczreplace UJudg with Arrange commit | commitdiff
2011-03-21 Adam Megaczmake StrongAlt a parameter rather than field in StrongC... commit | commitdiff
2011-03-20 Adam Megaczremove vec2list_injective commit | commitdiff
2011-03-20 Adam Megaczget rid of a bunch of admits in HaskStrongToProof commit | commitdiff
2011-03-20 Adam Megaczrequire all branches of LetRec be at the same level... commit | commitdiff
2011-03-16 Adam Megaczadd EGlobal/RGlobal for CoreVars whose binder we cannot see commit | commitdiff
2011-03-15 Adam Megaczreshuffle definitions in an attempt to iron out inter... commit | commitdiff
2011-03-14 Adam Megaczclose numerous holes in HaskStrongToProof commit | commitdiff
2011-03-13 Adam Megaczrestore HaskWeakToStrong functionality that I broke... commit | commitdiff
2011-03-12 Adam MegaczMake the HaskStrong type representation Kind-indexed... commit | commitdiff
2011-03-07 Adam Megaczadd HaskStrongToProof commit | commitdiff
Coq proofs and code accompanying the HetMet extensions for GHC