fix bugs in Unify.hs, store unifiers in fully-resolved form

very rudimentary support for feedback in GArrowTikZ

add support for flattening recursive-let

fix bugs in BiGArrow

update for new GHC coercion representation

remove RLet and RWhere

let RCut take a left environment as well

use -fsimpleopt-before-flatten in sanity checks

remove RJoin rule

better error reporting in coreTypeToWeakType; dont use Prelude_error

Makefile: use a for-loop to compile sanity checks

add "sanity" target to Makefile

add -fflatten and -funsafe-skolemize flags

add RCut, RLeft, RRight rules

rename constructors of Arrange to start with A instead of R

move more arrange routines into NaturalDeductionContext

move Arrange into NaturalDeductionContext

migrate HaskStrong away from using LeveledHaskType

HaskProof: make the succedent level part of the judgment

update Demo.hs

add commented-out/incomplete implementation of simplifyWeakExpr

General.v: add boolean and/or functions

rename variables to avoid Coq pickiness during extraction

partial support for LetRec in flattener

fix types of GAS_loop{l,r}

add new Where rule, eliminate unnecessary ga_swaps in the Skolemizer

note to self in HaskWeak

NaturalDeduction: add nd_exch

HaskFlattener: support escapifying multi-leaf contexts

complete rewrite of GArrowTikZ, update examples

GArrowSkeleton: add some more optimization cases

GArrowPortShape: add detectShape

Unify.hs: commenting fix

add begin/end{preview} to tex output

GArrowTikZ: improve pdf page cropping

update demo for new more-efficient encoding of functions

more efficient encoding of function types

add an identity production for Arrange

update demo

add GArrowPortShape

add GArrowSkeleton

fix bug in flattener, make extensionality axiom explicit

update examples

integrate skolemization pass with flattening

improve detection of type function kinds, mainly their saturation needs

add split_list to General.v

add ToString instance for lists

first draft of skolemization pass

add EqDecidable instances for option and Tree

swap order of hypotheses in RApp to match RLet

rewrite {take,drop}_arg_types to avoid use of equality proofs

HaskFlattener: represent first-order abstraction using GArrows

HaskFlattener: use ga_mk_raw

update PCF.v for new ECKind

HaskFlattener: simplify the flattener

HaskStrongTypes: add {take,drop}_arg_types

HaskFLattener: formatting fixes and refactoring

start using type-family-based GArrow classes

have Makefile check for coq 8.3pl2-tracer

add examples/.build to gitignore

add support for flattening non-recursive Let bindings

move general-purpose routines from HaskFlattener to HaskProof/General

split HaskLiteralsAndTyCons into two files

add support for hetmet_unflatten

add Demo.hs

make GArrowTikZ into a module rather than a standalone program

add support for hetmet_flatten casting variable

allow -fcoqpass to change the type of top-level bindings

use the "debug" version of Outputable for ToString in Coq code

change ECKind to *=>*=>*

abstract out the kind of environment classifiers (ECKind)

major improvements to flattener; almost finished now

allow rank-1 polymorphic types for globals

add PairTyCon and UnitTyCon

minor cleanups to Extraction-prefix.hs to eliminate warnings

further improvements to flattener

separate HaskProofStratified into PCF.v, HaskProgrammingLanguage.v, and HaskFlattener.v, major improvements to flattening algorithm

reorganize HaskProof files

clean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files

remove many [[admit]]s from HaskProofFlattener.v

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

prove all [admit]ted lemmas in HaskStrongToProof (not necessarily elegantly!)

add Makefile target for tikz demo

add examples/Makefile

add -fno-warn-unused-{binds,patterns} to Coq extraction

update GArrowTikZ.hs; still not finished, though

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