remove ClosedSIND (use "SIND []" instead)

remove all admits from ProgrammingLanguage.v

NaturalDeduction: add nd_swap, nd_prod_split, and some tactics

add examples targets to Makefile

add Unify.hs to examples

speed up builds by removing some dependencies from ExtractionMain

fix erroneous conclusion to penultimate lemma

use the $(MAKE) variable so -j2 works

Merge branches 'master' and 'master' of git.megacz.com/coq-hetmet

unbreak lots more stuff

uncomment some code in ProgrammingLanguage.v

remove the very last admit (missing proof) from GeneralizedArrowFromReification

add skeleton of GArrowTikZ

separate CoqPass.hs from All.v in Makefile

fix bug in GeneralizedArrowFromReification

All.v: uncomment things

bugfix in ReificationsIsomorphicToGeneralizedArrows

add commented-out definitions for analytic proofs and cut elimination

fill in lots of missing proofs

update to new coq-categories, base ND_Relation on inert sequences

remove notations from Preamble that come from coq-categories

update to account for coq-categories changes

fix Makefile bug

update submodule pointer, account for changes upstream

ExtractionMain: better pdflatex code output

re-arrange ProgrammingLanguage

add extra targets to Makefile

split HaskProofCategory into two files

remove unproven step1_lemma (it has a proof now)

formatting fixes

remove stale import from ExtractionMain

lots of cleanup

tweak comments in examples

reorganized examples directory

reorganize flattening code

HaskProofCategory: more work

swap the order of the hypotheses of RLet

NaturalDeduction: remove unnecessary scnd_leaf, add (s)cnd_property

add pushcheck

replace UJudg with Arrange

checkpoint

checkpoint

fix typo

ProgrammingLanguage: more implementation

HaskProofCategory: implement more

remove old code from WeakFunctorCategory

ReificationsIsomorphicToGeneralizedArrows: use EqDep

NaturalDeduction: allow multi-rule implementations for SequentExpansion and TreeStructuralRules

Merge branch 'master' of git.megacz.com/coq-hetmet

Conflicts:
src/Extraction-prefix.hs

organize Extraction-prefix.hs a bit

fallback plan: turn all CoreSyn coercions into unsafeCoerce

change name of string-extraction placeholder

remove PreCategory

Merge branch 'master' of git.megacz.com/coq-hetmet

uncomment more of the tutorial

update submodule pointer

almost finished with main theorem

fix -dont-load-proofs option in Makefile

checkpoint

get rid of vec_{fst,snd} axioms

improve error message

update submodule pointer

remove unnecessary comments

use WeakFunctorCategory to prove GArrow/Reification isomorphism

temporarily comment out

more bugfixes

fix {Reification,GeneralizedArrow}Category

improvements to ProgrammingLanguage

ProgrammingLanguage.v: add definitions for TypesL_{first,second}

finish definitions for SequentCalculus, CutRule, SequentExpansion

note that REmptyGroup and RLit are flat

update submodule pointer

update submodule pointer

re-arrange NaturalDeduction

change fst_zip/snd_zip to axioms

fix proof that Judgments(L) is Cartesian

add Concatenable, LatexMath, and fix HaskProofToLatex

add ToLatex instance for TyCon/TyFun

update categories submodule pointer

split Extraction.v so most can be compiled with -dont-load-proofs

HaskProofToLatex improvements

HaskProofCategory: add commented-out-code

use apply tactic in ReificationFromGeneralizedArrow; not sure why this is required

ProgrammingLanguage: significant cleanups

add LetRec case to Rule_Flat

NaturalDeductionCategory: cleanup, add SequentCalculus and CutRule

add ToLatex instance parameter to HaskStrong

remove unnecessary instance from HaskStrongTypes

change import order in HaskWeakVars

change import order in HaskCoreToWeak

add n-ary form of nd_weak

add ndr_void_proofs_irrelevant

move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons

add kindToLatex in HaskKinds

add ToLatex class, move machinery to General.v

add machinery to create merged Coq script GArrow.v

update categories submodule pointer

proofs that Types/Judgments form an enrichment

update tutorial for new GArrow classes

add distinctT, InT to General