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

2011-03-14	Adam Megacz	first pass at proper handling of coercions in HaskWeak	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	better error reporting in HaskWeakToStrong	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	better error reporting in Extraction.v	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	close numerous holes in HaskStrongToProof	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	major revision of HaskWeakToStrong, put phi/psi on...	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	fix spelling error in HaskWeakToCore	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	remove weakTypeOfWeakExpr and replaceWeakTypeVar, no...	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	store the scrutinee CoreVar in WeakExpr Case to simplify...	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	store the magic CoreVar for hetmet brak/esc in WeakExpr...	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	detect (->) TyCon and substitute FunTy in WeakToCore	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	fix bugs in LaTeX output	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	ToString instance for HaskCore	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	General.addErrorMessage, orErrorBindWithMessage	commit \| commitdiff \| tree
2011-03-14	Adam Megacz	move eol:string to General.v	commit \| commitdiff \| tree
2011-03-13	Adam Megacz	restore HaskWeakToStrong functionality that I broke...	commit \| commitdiff \| tree
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