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

eliminate ext_tree_{left,right} keywords

more formatting fixes

formatting fixes

minor cleanups, deleted dead code, eliminated use of (==) on CoreType

fix sortAlts so it actually does something

add tutorial.coqpass to gitignore

add tutorial to the repository

rename weakTypeToType'' to weakTypeToTypeOfKind

revise tyFunKind to use splitKind

add splitKind to HaskKind

fix ToString instance for Kind

minor cleanups in HaskStrongToWeak

include URL for trfrac.sty and mathpartir in LaTeX output

first pass at proper handling of coercions in HaskWeak

better error reporting in HaskWeakToStrong

better error reporting in Extraction.v

close numerous holes in HaskStrongToProof

major revision of HaskWeakToStrong, put phi/psi on the error monad

fix spelling error in HaskWeakToCore

remove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required

store the scrutinee CoreVar in WeakExpr Case to simplify WeakExprToCoreExpr

store the magic CoreVar for hetmet brak/esc in WeakExpr Esc/Brak