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

2011-04-27	Adam Megacz	prove all [admit]ted lemmas in HaskStrongToProof (not...	commit \| commitdiff \| tree \| snapshot
2011-04-25	Adam Megacz	update GArrowTikZ.hs; still not finished, though	commit \| commitdiff \| tree \| snapshot
2011-04-25	Adam Megacz	remove ClosedSIND (use "SIND []" instead)	commit \| commitdiff \| tree \| snapshot
2011-04-24	Adam Megacz	remove all admits from ProgrammingLanguage.v	commit \| commitdiff \| tree \| snapshot
2011-04-24	Adam Megacz	NaturalDeduction: add nd_swap, nd_prod_split, and some...	commit \| commitdiff \| tree \| snapshot
2011-04-24	Adam Megacz	add examples targets to Makefile	commit \| commitdiff \| tree \| snapshot
2011-04-24	Adam Megacz	add Unify.hs to examples	commit \| commitdiff \| tree \| snapshot
2011-04-18	Adam Megacz	speed up builds by removing some dependencies from...	commit \| commitdiff \| tree \| snapshot
2011-04-16	Adam Megacz	fix erroneous conclusion to penultimate lemma	commit \| commitdiff \| tree \| snapshot
2011-04-11	Adam Megacz	use the $(MAKE) variable so -j2 works	commit \| commitdiff \| tree \| snapshot
2011-04-11	Adam Megacz	Merge branches 'master' and 'master' of git.megacz...	commit \| commitdiff \| tree \| snapshot
2011-04-11	Adam Megacz	unbreak lots more stuff	commit \| commitdiff \| tree \| snapshot
2011-04-11	Adam Megacz	uncomment some code in ProgrammingLanguage.v	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	remove the very last admit (missing proof) from General...	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	add skeleton of GArrowTikZ	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	separate CoqPass.hs from All.v in Makefile	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	fix bug in GeneralizedArrowFromReification	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	All.v: uncomment things	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	bugfix in ReificationsIsomorphicToGeneralizedArrows	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	add commented-out definitions for analytic proofs and...	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	fill in lots of missing proofs	commit \| commitdiff \| tree \| snapshot
2011-04-10	Adam Megacz	update to new coq-categories, base ND_Relation on inert...	commit \| commitdiff \| tree \| snapshot
2011-04-09	Adam Megacz	remove notations from Preamble that come from coq-categ...	commit \| commitdiff \| tree \| snapshot
2011-04-04	Adam Megacz	update to account for coq-categories changes	commit \| commitdiff \| tree \| snapshot
2011-04-02	Adam Megacz	fix Makefile bug	commit \| commitdiff \| tree \| snapshot
2011-04-02	Adam Megacz	update submodule pointer, account for changes upstream	commit \| commitdiff \| tree \| snapshot
2011-04-02	Adam Megacz	ExtractionMain: better pdflatex code output	commit \| commitdiff \| tree \| snapshot
2011-04-02	Adam Megacz	re-arrange ProgrammingLanguage	commit \| commitdiff \| tree \| snapshot
2011-04-02	Adam Megacz	add extra targets to Makefile	commit \| commitdiff \| tree \| snapshot
2011-04-02	Adam Megacz	split HaskProofCategory into two files	commit \| commitdiff \| tree \| snapshot
2011-04-01	Adam Megacz	remove unproven step1_lemma (it has a proof now)	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	formatting fixes	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	remove stale import from ExtractionMain	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	lots of cleanup	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	tweak comments in examples	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	reorganized examples directory	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	reorganize flattening code	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	HaskProofCategory: more work	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	swap the order of the hypotheses of RLet	commit \| commitdiff \| tree \| snapshot
2011-03-29	Adam Megacz	NaturalDeduction: remove unnecessary scnd_leaf, add...	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	add pushcheck	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	replace UJudg with Arrange	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	checkpoint	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	checkpoint	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	fix typo	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	ProgrammingLanguage: more implementation	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	HaskProofCategory: implement more	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	remove old code from WeakFunctorCategory	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	ReificationsIsomorphicToGeneralizedArrows: use EqDep	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	NaturalDeduction: allow multi-rule implementations...	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	Merge branch 'master' of git.megacz.com/coq-hetmet	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	organize Extraction-prefix.hs a bit	commit \| commitdiff \| tree \| snapshot
2011-03-28	Adam Megacz	fallback plan: turn all CoreSyn coercions into unsafeCoerce	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	change name of string-extraction placeholder	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	remove PreCategory	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	Merge branch 'master' of git.megacz.com/coq-hetmet	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	uncomment more of the tutorial	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	update submodule pointer	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	almost finished with main theorem	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	fix -dont-load-proofs option in Makefile	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	checkpoint	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	get rid of vec_{fst,snd} axioms	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	improve error message	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	update submodule pointer	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	remove unnecessary comments	commit \| commitdiff \| tree \| snapshot
2011-03-27	Adam Megacz	use WeakFunctorCategory to prove GArrow/Reification...	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	temporarily comment out	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	more bugfixes	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	fix {Reification,GeneralizedArrow}Category	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	improvements to ProgrammingLanguage	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	ProgrammingLanguage.v: add definitions for TypesL_...	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	finish definitions for SequentCalculus, CutRule, Sequen...	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	note that REmptyGroup and RLit are flat	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	update submodule pointer	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	update submodule pointer	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	re-arrange NaturalDeduction	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	change fst_zip/snd_zip to axioms	commit \| commitdiff \| tree \| snapshot
2011-03-26	Adam Megacz	fix proof that Judgments(L) is Cartesian	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add Concatenable, LatexMath, and fix HaskProofToLatex	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add ToLatex instance for TyCon/TyFun	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	update categories submodule pointer	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	split Extraction.v so most can be compiled with -dont...	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	HaskProofToLatex improvements	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	HaskProofCategory: add commented-out-code	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	use apply tactic in ReificationFromGeneralizedArrow...	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	ProgrammingLanguage: significant cleanups	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add LetRec case to Rule_Flat	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	NaturalDeductionCategory: cleanup, add SequentCalculus...	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add ToLatex instance parameter to HaskStrong	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	remove unnecessary instance from HaskStrongTypes	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	change import order in HaskWeakVars	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	change import order in HaskCoreToWeak	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add n-ary form of nd_weak	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add ndr_void_proofs_irrelevant	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add kindToLatex in HaskKinds	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add ToLatex class, move machinery to General.v	commit \| commitdiff \| tree \| snapshot
2011-03-25	Adam Megacz	add machinery to create merged Coq script GArrow.v	commit \| commitdiff \| tree \| snapshot
2011-03-22	Adam Megacz	update categories submodule pointer	commit \| commitdiff \| tree \| snapshot
2011-03-22	Adam Megacz	proofs that Types/Judgments form an enrichment	commit \| commitdiff \| tree \| snapshot
next

Coq proofs and code accompanying the HetMet extensions for GHC

RSS Atom