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
2011-03-15 Adam Megaczformatting
2011-03-15 Adam Megaczchange names of Kind constructors to be more informative
2011-03-15 Adam Megaczreshuffle definitions in an attempt to iron out inter...
2011-03-14 Adam Megaczadd support for CSP in HaskCore+HaskWeak
2011-03-14 Adam Megaczremove dead code from HaskWeak
2011-03-14 Adam Megaczeliminate ext_tree_{left,right} keywords
2011-03-14 Adam Megaczmore formatting fixes
2011-03-14 Adam Megaczformatting fixes
2011-03-14 Adam Megaczminor cleanups, deleted dead code, eliminated use of...
2011-03-14 Adam Megaczfix sortAlts so it actually does something
2011-03-14 Adam Megaczadd tutorial.coqpass to gitignore
2011-03-14 Adam Megaczadd tutorial to the repository
2011-03-14 Adam Megaczrename weakTypeToType'' to weakTypeToTypeOfKind
2011-03-14 Adam Megaczrevise tyFunKind to use splitKind
2011-03-14 Adam Megaczadd splitKind to HaskKind
2011-03-14 Adam Megaczfix ToString instance for Kind
2011-03-14 Adam Megaczminor cleanups in HaskStrongToWeak
2011-03-14 Adam Megaczinclude URL for trfrac.sty and mathpartir in LaTeX...
2011-03-14 Adam Megaczfirst pass at proper handling of coercions in HaskWeak
2011-03-14 Adam Megaczbetter error reporting in HaskWeakToStrong
2011-03-14 Adam Megaczbetter error reporting in Extraction.v
2011-03-14 Adam Megaczclose numerous holes in HaskStrongToProof
2011-03-14 Adam Megaczmajor revision of HaskWeakToStrong, put phi/psi on...
2011-03-14 Adam Megaczfix spelling error in HaskWeakToCore
2011-03-14 Adam Megaczremove weakTypeOfWeakExpr and replaceWeakTypeVar, no...
2011-03-14 Adam Megaczstore the scrutinee CoreVar in WeakExpr Case to simplif...
2011-03-14 Adam Megaczstore the magic CoreVar for hetmet brak/esc in WeakExpr...
2011-03-14 Adam Megaczdetect (->) TyCon and substitute FunTy in WeakToCore
2011-03-14 Adam Megaczfix bugs in LaTeX output
2011-03-14 Adam MegaczToString instance for HaskCore
2011-03-14 Adam MegaczGeneral.addErrorMessage, orErrorBindWithMessage
2011-03-14 Adam Megaczmove eol:string to General.v
2011-03-13 Adam Megaczrestore HaskWeakToStrong functionality that I broke...
2011-03-13 Adam MegaczRemove unnecessary coreVar_eq_refl axiom
2011-03-13 Adam MegaczRename to Extraction.Prelude_error
2011-03-13 Adam MegaczEliminate the need for WeakVar decidable equality axiom
2011-03-12 Adam Megaczupdate push-url in Makefile
2011-03-12 Adam MegaczMake the HaskStrong type representation Kind-indexed...
2011-03-09 Adam Megaczmore Makefile updates
2011-03-07 Adam MegaczMakefile updates
2011-03-07 Adam Megaczmake latex output use the preview package to set the...
2011-03-07 Adam Megaczadd HaskProofToStrong skeleton implementation
2011-03-07 Adam Megaczadd HaskStrongToWeak
2011-03-07 Adam Megaczadd HaskStrongToProof
2011-03-07 Adam Megaczadd HaskWeakToStrong
2011-03-07 Adam Megaczgive HaskWeak its own type representation, fix numerous...
2011-03-07 Adam Megaczbetter names for the auxiliary CaseBranch records
2011-03-07 Adam Megaczseparate type/coer/expr variables in HaskWeak case...
2011-03-07 Adam Megaczstore variables in ELetRecBindings rather than its...
2011-03-07 Adam Megaczadd HaskWeakToCore
2011-03-07 Adam Megaczadd proper proofs of the fact that every rule has exact...
2011-03-07 Adam MegaczChanged WEBrak/WEEsc to store a CoreType
2011-03-07 Adam MegaczAdded WeakVar, a separate variable representation for...
2011-03-07 Adam Megaczadded "publish" target to regenerate tex/pdf code
2011-03-07 Adam Megaczadded HaskCoreToWeak
2011-03-07 Adam Megaczcleaned up lots of FIXMEs in ProofToLatex
2011-03-02 Adam MegaczInitial checkin of Coq-in-GHC code