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

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
2011-03-22	Adam Megacz	update tutorial for new GArrow classes	commit \| commitdiff \| tree \| snapshot
2011-03-21	Adam Megacz	add distinctT, InT to General	commit \| commitdiff \| tree \| snapshot
2011-03-21	Adam Megacz	add HaskXXXXCategory, generalized arrows, and reifications	commit \| commitdiff \| tree \| snapshot
2011-03-21	Adam Megacz	add coq-categories as a submodule	commit \| commitdiff \| tree \| snapshot
2011-03-21	Adam Megacz	comment out portions of the tutorial which do not yet...	commit \| commitdiff \| tree \| snapshot
2011-03-21	Adam Megacz	Makefile update	commit \| commitdiff \| tree \| snapshot
2011-03-21	Adam Megacz	make StrongAlt a parameter rather than field in StrongC...	commit \| commitdiff \| tree \| snapshot
2011-03-20	Adam Megacz	remove vec2list_injective	commit \| commitdiff \| tree \| snapshot
2011-03-20	Adam Megacz	get rid of a bunch of admits in HaskStrongToProof	commit \| commitdiff \| tree \| snapshot
2011-03-20	Adam Megacz	require all branches of LetRec be at the same level...	commit \| commitdiff \| tree \| snapshot
2011-03-20	Adam Megacz	add mapOptionTree_extensional, leaves_unleaves, mapleaves	commit \| commitdiff \| tree \| snapshot
2011-03-20	Adam Megacz	add distinct_decidable, in_decidable to General.v	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	checkpoint	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	improve HaskProofToStrong, although its messier now	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	add tracing support to Extraction-prefix.hs	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	add mapleaves to General.v	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	change LetRec rule to allow only a single expression...	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	add ToString instance for HaskStrong	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	add closedNDtoNormalND to NaturalDeduction	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	add UniqMonad	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	add itmap and itree_to_tree	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	add treeToString method to General	commit \| commitdiff \| tree \| snapshot
2011-03-19	Adam Megacz	move Prelude_error to General.v	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	expand tutorial.hs, include justification for scoping...	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	check for Case that uses its binder, which we do not...	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	Makefile fixes: ignore emacs droppings	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	fix broken sortAlts implementation	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	major overhaul of WeakToStrong/StrongToWeak; it can...	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	better variable names in HaskWeakToCore	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	restrict RNote to one hypothesis, major additions to...	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	add EGlobal/RGlobal for CoreVars whose binder we cannot see	commit \| commitdiff \| tree \| snapshot
2011-03-16	Adam Megacz	add crude Monad type class	commit \| commitdiff \| tree \| snapshot
2011-03-15	Adam Megacz	final batch of fixups before enabling -fcoqpass	commit \| commitdiff \| tree \| snapshot
2011-03-15	Adam Megacz	fix spellings in Extraction-prefix.hs, minor tweaks	commit \| commitdiff \| tree \| snapshot
2011-03-15	Adam Megacz	formatting	commit \| commitdiff \| tree \| snapshot
2011-03-15	Adam Megacz	change names of Kind constructors to be more informative	commit \| commitdiff \| tree \| snapshot
2011-03-15	Adam Megacz	reshuffle definitions in an attempt to iron out inter...	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	add support for CSP in HaskCore+HaskWeak	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	remove dead code from HaskWeak	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	eliminate ext_tree_{left,right} keywords	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	more formatting fixes	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	formatting fixes	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	minor cleanups, deleted dead code, eliminated use of...	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	fix sortAlts so it actually does something	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	add tutorial.coqpass to gitignore	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	add tutorial to the repository	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	rename weakTypeToType'' to weakTypeToTypeOfKind	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	revise tyFunKind to use splitKind	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	add splitKind to HaskKind	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	fix ToString instance for Kind	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	minor cleanups in HaskStrongToWeak	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	include URL for trfrac.sty and mathpartir in LaTeX...	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	first pass at proper handling of coercions in HaskWeak	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	better error reporting in HaskWeakToStrong	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	better error reporting in Extraction.v	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	close numerous holes in HaskStrongToProof	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	major revision of HaskWeakToStrong, put phi/psi on...	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	fix spelling error in HaskWeakToCore	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	remove weakTypeOfWeakExpr and replaceWeakTypeVar, no...	commit \| commitdiff \| tree \| snapshot
2011-03-14	Adam Megacz	store the scrutinee CoreVar in WeakExpr Case to simplif...	commit \| commitdiff \| tree \| snapshot
next

Coq proofs and code accompanying the HetMet extensions for GHC

RSS Atom