coq-hetmet.git
2011-05-10 Adam Megaczstart using type-family-based GArrow classes
2011-05-10 Adam Megaczhave Makefile check for coq 8.3pl2-tracer
2011-05-10 Adam Megaczadd examples/.build to gitignore
2011-05-10 Adam Megaczadd support for flattening non-recursive Let bindings
2011-05-09 Adam Megaczmove general-purpose routines from HaskFlattener to...
2011-05-09 Adam Megaczsplit HaskLiteralsAndTyCons into two files
2011-05-09 Adam Megaczadd support for hetmet_unflatten
2011-05-09 Adam Megaczadd Demo.hs
2011-05-09 Adam Megaczmake GArrowTikZ into a module rather than a standalone...
2011-05-09 Adam Megaczadd support for hetmet_flatten casting variable
2011-05-09 Adam Megaczallow -fcoqpass to change the type of top-level bindings
2011-05-09 Adam Megaczuse the "debug" version of Outputable for ToString...
2011-05-09 Adam Megaczchange ECKind to *=>*=>*
2011-05-09 Adam Megaczabstract out the kind of environment classifiers (ECKind)
2011-05-09 Adam Megaczmajor improvements to flattener; almost finished now
2011-05-09 Adam Megaczallow rank-1 polymorphic types for globals
2011-05-09 Adam Megaczadd PairTyCon and UnitTyCon
2011-05-09 Adam Megaczminor cleanups to Extraction-prefix.hs to eliminate...
2011-05-05 Adam Megaczfurther improvements to flattener
2011-05-03 Adam Megaczseparate HaskProofStratified into PCF.v, HaskProgrammin...
2011-04-30 Adam Megaczreorganize HaskProof files
2011-04-30 Adam Megaczclean up hints for NaturalDeduction, split ProgrammingL...
2011-04-29 Adam Megaczremove many [[admit]]s from HaskProofFlattener.v
2011-04-27 Adam MegaczMerge branch 'master' of git.megacz.com/coq-hetmet
2011-04-27 Adam Megaczprove all [admit]ted lemmas in HaskStrongToProof (not...
2011-04-26 Adam Megaczadd Makefile target for tikz demo
2011-04-26 Adam Megaczadd examples/Makefile
2011-04-25 Adam Megaczadd -fno-warn-unused-{binds,patterns} to Coq extraction
2011-04-25 Adam Megaczupdate GArrowTikZ.hs; still not finished, though
2011-04-25 Adam Megaczremove ClosedSIND (use "SIND []" instead)
2011-04-24 Adam Megaczremove all admits from ProgrammingLanguage.v
2011-04-24 Adam MegaczNaturalDeduction: add nd_swap, nd_prod_split, and some...
2011-04-24 Adam Megaczadd examples targets to Makefile
2011-04-24 Adam Megaczadd Unify.hs to examples
2011-04-18 Adam Megaczspeed up builds by removing some dependencies from...
2011-04-16 Adam Megaczfix erroneous conclusion to penultimate lemma
2011-04-11 Adam Megaczuse the $(MAKE) variable so -j2 works
2011-04-11 Adam MegaczMerge branches 'master' and 'master' of git.megacz...
2011-04-11 Adam Megaczunbreak lots more stuff
2011-04-11 Adam Megaczuncomment some code in ProgrammingLanguage.v
2011-04-10 Adam Megaczremove the very last admit (missing proof) from General...
2011-04-10 Adam Megaczadd skeleton of GArrowTikZ
2011-04-10 Adam Megaczseparate CoqPass.hs from All.v in Makefile
2011-04-10 Adam Megaczfix bug in GeneralizedArrowFromReification
2011-04-10 Adam MegaczAll.v: uncomment things
2011-04-10 Adam Megaczbugfix in ReificationsIsomorphicToGeneralizedArrows
2011-04-10 Adam Megaczadd commented-out definitions for analytic proofs and...
2011-04-10 Adam Megaczfill in lots of missing proofs
2011-04-10 Adam Megaczupdate to new coq-categories, base ND_Relation on inert...
2011-04-09 Adam Megaczremove notations from Preamble that come from coq-categ...
2011-04-04 Adam Megaczupdate to account for coq-categories changes
2011-04-02 Adam Megaczfix Makefile bug
2011-04-02 Adam Megaczupdate submodule pointer, account for changes upstream
2011-04-02 Adam MegaczExtractionMain: better pdflatex code output
2011-04-02 Adam Megaczre-arrange ProgrammingLanguage
2011-04-02 Adam Megaczadd extra targets to Makefile
2011-04-02 Adam Megaczsplit HaskProofCategory into two files
2011-04-01 Adam Megaczremove unproven step1_lemma (it has a proof now)
2011-03-29 Adam Megaczformatting fixes
2011-03-29 Adam Megaczremove stale import from ExtractionMain
2011-03-29 Adam Megaczlots of cleanup
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 git.megacz.com/coq-hetmet
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 git.megacz.com/coq-hetmet
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
next