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

add HaskXXXXCategory, generalized arrows, and reifications

add coq-categories as a submodule

comment out portions of the tutorial which do not yet work due to GHC.Prim.Any

Makefile update

make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch

remove vec2list_injective

get rid of a bunch of admits in HaskStrongToProof

require all branches of LetRec be at the same level in HaskProof

add mapOptionTree_extensional, leaves_unleaves, mapleaves

add distinct_decidable, in_decidable to General.v

checkpoint

improve HaskProofToStrong, although its messier now

add tracing support to Extraction-prefix.hs

add mapleaves to General.v

change LetRec rule to allow only a single expression in the body

add ToString instance for HaskStrong

add closedNDtoNormalND to NaturalDeduction

add UniqMonad

add itmap and itree_to_tree

add treeToString method to General

move Prelude_error to General.v

expand tutorial.hs, include justification for scoping changes

check for Case that uses its binder, which we do not support

Makefile fixes: ignore emacs droppings

fix broken sortAlts implementation

major overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial

better variable names in HaskWeakToCore

restrict RNote to one hypothesis, major additions to ProofToStrong

add EGlobal/RGlobal for CoreVars whose binder we cannot see

add crude Monad type class

final batch of fixups before enabling -fcoqpass

fix spellings in Extraction-prefix.hs, minor tweaks

formatting

change names of Kind constructors to be more informative

reshuffle definitions in an attempt to iron out inter-file dependenceies

add support for CSP in HaskCore+HaskWeak

remove dead code from HaskWeak