2011-03-29 Adam Megacztweak comments in examples
2011-03-29 Adam Megaczreorganized examples directory
2011-03-29 Adam Megaczreorganize flattening code
2011-03-29 Adam MegaczHaskProofCategory: more work
2011-03-29 Adam Megaczswap the order of the hypotheses of RLet
2011-03-29 Adam MegaczNaturalDeduction: remove unnecessary scnd_leaf, add...
2011-03-28 Adam Megaczadd pushcheck
2011-03-28 Adam Megaczreplace UJudg with Arrange
2011-03-28 Adam Megaczcheckpoint
2011-03-28 Adam Megaczcheckpoint
2011-03-28 Adam Megaczfix typo
2011-03-28 Adam MegaczProgrammingLanguage: more implementation
2011-03-28 Adam MegaczHaskProofCategory: implement more
2011-03-28 Adam Megaczremove old code from WeakFunctorCategory
2011-03-28 Adam MegaczReificationsIsomorphicToGeneralizedArrows: use EqDep
2011-03-28 Adam MegaczNaturalDeduction: allow multi-rule implementations...
2011-03-28 Adam MegaczMerge branch 'master' of
2011-03-28 Adam Megaczorganize Extraction-prefix.hs a bit
2011-03-28 Adam Megaczfallback plan: turn all CoreSyn coercions into unsafeCoerce
2011-03-27 Adam Megaczchange name of string-extraction placeholder
2011-03-27 Adam Megaczremove PreCategory
2011-03-27 Adam MegaczMerge branch 'master' of
2011-03-27 Adam Megaczuncomment more of the tutorial
2011-03-27 Adam Megaczupdate submodule pointer
2011-03-27 Adam Megaczalmost finished with main theorem
2011-03-27 Adam Megaczfix -dont-load-proofs option in Makefile
2011-03-27 Adam Megaczcheckpoint
2011-03-27 Adam Megaczget rid of vec_{fst,snd} axioms
2011-03-27 Adam Megaczimprove error message
2011-03-27 Adam Megaczupdate submodule pointer
2011-03-27 Adam Megaczremove unnecessary comments
2011-03-27 Adam Megaczuse WeakFunctorCategory to prove GArrow/Reification...
2011-03-26 Adam Megacztemporarily comment out
2011-03-26 Adam Megaczmore bugfixes
2011-03-26 Adam Megaczfix {Reification,GeneralizedArrow}Category
2011-03-26 Adam Megaczimprovements to ProgrammingLanguage
2011-03-26 Adam MegaczProgrammingLanguage.v: add definitions for TypesL_...
2011-03-26 Adam Megaczfinish definitions for SequentCalculus, CutRule, Sequen...
2011-03-26 Adam Megacznote that REmptyGroup and RLit are flat
2011-03-26 Adam Megaczupdate submodule pointer
2011-03-26 Adam Megaczupdate submodule pointer
2011-03-26 Adam Megaczre-arrange NaturalDeduction
2011-03-26 Adam Megaczchange fst_zip/snd_zip to axioms
2011-03-26 Adam Megaczfix proof that Judgments(L) is Cartesian
2011-03-25 Adam Megaczadd Concatenable, LatexMath, and fix HaskProofToLatex
2011-03-25 Adam Megaczadd ToLatex instance for TyCon/TyFun
2011-03-25 Adam Megaczupdate categories submodule pointer
2011-03-25 Adam Megaczsplit Extraction.v so most can be compiled with -dont...
2011-03-25 Adam MegaczHaskProofToLatex improvements
2011-03-25 Adam MegaczHaskProofCategory: add commented-out-code
2011-03-25 Adam Megaczuse apply tactic in ReificationFromGeneralizedArrow...
2011-03-25 Adam MegaczProgrammingLanguage: significant cleanups
2011-03-25 Adam Megaczadd LetRec case to Rule_Flat
2011-03-25 Adam MegaczNaturalDeductionCategory: cleanup, add SequentCalculus...
2011-03-25 Adam Megaczadd ToLatex instance parameter to HaskStrong
2011-03-25 Adam Megaczremove unnecessary instance from HaskStrongTypes
2011-03-25 Adam Megaczchange import order in HaskWeakVars
2011-03-25 Adam Megaczchange import order in HaskCoreToWeak
2011-03-25 Adam Megaczadd n-ary form of nd_weak
2011-03-25 Adam Megaczadd ndr_void_proofs_irrelevant
2011-03-25 Adam Megaczmove ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons
2011-03-25 Adam Megaczadd kindToLatex in HaskKinds
2011-03-25 Adam Megaczadd ToLatex class, move machinery to General.v
2011-03-25 Adam Megaczadd machinery to create merged Coq script GArrow.v
2011-03-22 Adam Megaczupdate categories submodule pointer
2011-03-22 Adam Megaczproofs that Types/Judgments form an enrichment
2011-03-22 Adam Megaczupdate tutorial for new GArrow classes
2011-03-21 Adam Megaczadd distinctT, InT to General
2011-03-21 Adam Megaczadd HaskXXXXCategory, generalized arrows, and reifications
2011-03-21 Adam Megaczadd coq-categories as a submodule
2011-03-21 Adam Megaczcomment out portions of the tutorial which do not yet...
2011-03-21 Adam MegaczMakefile update
2011-03-21 Adam Megaczmake StrongAlt a parameter rather than field in StrongC...
2011-03-20 Adam Megaczremove vec2list_injective
2011-03-20 Adam Megaczget rid of a bunch of admits in HaskStrongToProof
2011-03-20 Adam Megaczrequire all branches of LetRec be at the same level...
2011-03-20 Adam Megaczadd mapOptionTree_extensional, leaves_unleaves, mapleaves
2011-03-20 Adam Megaczadd distinct_decidable, in_decidable to General.v
2011-03-19 Adam Megaczcheckpoint
2011-03-19 Adam Megaczimprove HaskProofToStrong, although its messier now
2011-03-19 Adam Megaczadd tracing support to Extraction-prefix.hs
2011-03-19 Adam Megaczadd mapleaves to General.v
2011-03-19 Adam Megaczchange LetRec rule to allow only a single expression...
2011-03-19 Adam Megaczadd ToString instance for HaskStrong
2011-03-19 Adam Megaczadd closedNDtoNormalND to NaturalDeduction
2011-03-19 Adam Megaczadd UniqMonad
2011-03-19 Adam Megaczadd itmap and itree_to_tree
2011-03-19 Adam Megaczadd treeToString method to General
2011-03-19 Adam Megaczmove Prelude_error to General.v
2011-03-16 Adam Megaczexpand tutorial.hs, include justification for scoping...
2011-03-16 Adam Megaczcheck for Case that uses its binder, which we do not...
2011-03-16 Adam MegaczMakefile fixes: ignore emacs droppings
2011-03-16 Adam Megaczfix broken sortAlts implementation
2011-03-16 Adam Megaczmajor overhaul of WeakToStrong/StrongToWeak; it can...
2011-03-16 Adam Megaczbetter variable names in HaskWeakToCore
2011-03-16 Adam Megaczrestrict RNote to one hypothesis, major additions to...
2011-03-16 Adam Megaczadd EGlobal/RGlobal for CoreVars whose binder we cannot see
2011-03-16 Adam Megaczadd crude Monad type class
2011-03-15 Adam Megaczfinal batch of fixups before enabling -fcoqpass
2011-03-15 Adam Megaczfix spellings in Extraction-prefix.hs, minor tweaks