git.megacz.com Git - coq-hetmet.git/search

2011-03-13	Adam Megacz	Remove unnecessary coreVar_eq_refl axiom	commit \| commitdiff \| tree
2011-03-13	Adam Megacz	Rename Extraction.fail to Extraction.Prelude_error	commit \| commitdiff \| tree
2011-03-13	Adam Megacz	Eliminate the need for WeakVar decidable equality axiom	commit \| commitdiff \| tree
2011-03-12	Adam Megacz	Make the HaskStrong type representation Kind-indexed...	commit \| commitdiff \| tree
2011-03-09	Adam Megacz	more Makefile updates	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	Makefile updates	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	make latex output use the preview package to set the...	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	add HaskProofToStrong skeleton implementation	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	add HaskStrongToWeak	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	add HaskStrongToProof	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	add HaskWeakToStrong	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	give HaskWeak its own type representation, fix numerous...	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	better names for the auxiliary CaseBranch records	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	separate type/coer/expr variables in HaskWeak case...	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	store variables in ELetRecBindings rather than its...	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	add HaskWeakToCore	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	add proper proofs of the fact that every rule has exactly...	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	Changed WEBrak/WEEsc to store a CoreType	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	Added WeakVar, a separate variable representation for...	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	added "publish" target to regenerate tex/pdf code	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	added HaskCoreToWeak	commit \| commitdiff \| tree
2011-03-07	Adam Megacz	cleaned up lots of FIXMEs in ProofToLatex	commit \| commitdiff \| tree
2011-03-02	Adam Megacz	Initial checkin of Coq-in-GHC code	commit \| commitdiff \| tree

Coq proofs and code accompanying the HetMet extensions for GHC

RSS Atom