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

[coq-hetmet.git] / src / HaskStrongToWeak.v

2011-04-27	Adam Megacz	prove all [admit]ted lemmas in HaskStrongToProof (not...	blob \| commitdiff
2011-03-29	Adam Megacz	lots of cleanup	blob \| commitdiff \| diff to current
2011-03-25	Adam Megacz	add Concatenable, LatexMath, and fix HaskProofToLatex	blob \| commitdiff \| diff to current
2011-03-21	Adam Megacz	make StrongAlt a parameter rather than field in StrongC...	blob \| commitdiff \| diff to current
2011-03-20	Adam Megacz	require all branches of LetRec be at the same level...	blob \| commitdiff \| diff to current
2011-03-19	Adam Megacz	add UniqMonad	blob \| commitdiff \| diff to current
2011-03-16	Adam Megacz	major overhaul of WeakToStrong/StrongToWeak; it can...	blob \| commitdiff \| diff to current
2011-03-15	Adam Megacz	final batch of fixups before enabling -fcoqpass	blob \| commitdiff \| diff to current
2011-03-15	Adam Megacz	fix spellings in Extraction-prefix.hs, minor tweaks	blob \| commitdiff \| diff to current
2011-03-15	Adam Megacz	reshuffle definitions in an attempt to iron out inter...	blob \| commitdiff \| diff to current
2011-03-14	Adam Megacz	minor cleanups in HaskStrongToWeak	blob \| commitdiff \| diff to current
2011-03-14	Adam Megacz	major revision of HaskWeakToStrong, put phi/psi on...	blob \| commitdiff \| diff to current
2011-03-14	Adam Megacz	store the scrutinee CoreVar in WeakExpr Case to simplif...	blob \| commitdiff \| diff to current
2011-03-14	Adam Megacz	store the magic CoreVar for hetmet brak/esc in WeakExpr...	blob \| commitdiff \| diff to current
2011-03-13	Adam Megacz	restore HaskWeakToStrong functionality that I broke...	blob \| commitdiff \| diff to current
2011-03-13	Adam Megacz	Eliminate the need for WeakVar decidable equality axiom	blob \| commitdiff \| diff to current
2011-03-12	Adam Megacz	Make the HaskStrong type representation Kind-indexed...	blob \| commitdiff \| diff to current
2011-03-07	Adam Megacz	add HaskStrongToWeak	blob \| commitdiff \| diff to current

Coq proofs and code accompanying the HetMet extensions for GHC

RSS Atom