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

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

2011-04-30	Adam Megacz	clean up hints for NaturalDeduction, split ProgrammingL...	blob \| commitdiff
2011-04-24	Adam Megacz	remove all admits from ProgrammingLanguage.v	blob \| commitdiff \| diff to current
2011-04-11	Adam Megacz	unbreak lots more stuff	blob \| commitdiff \| diff to current
2011-04-11	Adam Megacz	uncomment some code in ProgrammingLanguage.v	blob \| commitdiff \| diff to current
2011-04-10	Adam Megacz	fill in lots of missing proofs	blob \| commitdiff \| diff to current
2011-04-10	Adam Megacz	update to new coq-categories, base ND_Relation on inert...	blob \| commitdiff \| diff to current
2011-04-04	Adam Megacz	update to account for coq-categories changes	blob \| commitdiff \| diff to current
2011-04-02	Adam Megacz	update submodule pointer, account for changes upstream	blob \| commitdiff \| diff to current
2011-03-29	Adam Megacz	lots of cleanup	blob \| commitdiff \| diff to current
2011-03-28	Adam Megacz	fix typo	blob \| commitdiff \| diff to current
2011-03-28	Adam Megacz	ProgrammingLanguage: more implementation	blob \| commitdiff \| diff to current
2011-03-27	Adam Megacz	remove unnecessary comments	blob \| commitdiff \| diff to current
2011-03-26	Adam Megacz	improvements to ProgrammingLanguage	blob \| commitdiff \| diff to current
2011-03-26	Adam Megacz	ProgrammingLanguage.v: add definitions for TypesL_...	blob \| commitdiff \| diff to current
2011-03-26	Adam Megacz	re-arrange NaturalDeduction	blob \| commitdiff \| diff to current
2011-03-26	Adam Megacz	fix proof that Judgments(L) is Cartesian	blob \| commitdiff \| diff to current
2011-03-25	Adam Megacz	ProgrammingLanguage: significant cleanups	blob \| commitdiff \| diff to current
2011-03-22	Adam Megacz	proofs that Types/Judgments form an enrichment	blob \| commitdiff \| diff to current

Coq proofs and code accompanying the HetMet extensions for GHC

RSS Atom