projects / coq-hetmet.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
coq-hetmet.git
2011-03-19 Adam Megaczchange LetRec rule to allow only a single expression... commit | commitdiff | tree | snapshot
2011-03-19 Adam Megaczadd ToString instance for HaskStrong commit | commitdiff | tree | snapshot
2011-03-19 Adam Megaczadd closedNDtoNormalND to NaturalDeduction commit | commitdiff | tree | snapshot
2011-03-19 Adam Megaczadd UniqMonad commit | commitdiff | tree | snapshot
2011-03-19 Adam Megaczadd itmap and itree_to_tree commit | commitdiff | tree | snapshot
2011-03-19 Adam Megaczadd treeToString method to General commit | commitdiff | tree | snapshot
2011-03-19 Adam Megaczmove Prelude_error to General.v commit | commitdiff | tree | snapshot
2011-03-16 Adam Megaczexpand tutorial.hs, include justification for scoping... commit | commitdiff | tree | snapshot
2011-03-16 Adam Megaczcheck for Case that uses its binder, which we do not... commit | commitdiff | tree | snapshot
2011-03-16 Adam MegaczMakefile fixes: ignore emacs droppings commit | commitdiff | tree | snapshot
2011-03-16 Adam Megaczfix broken sortAlts implementation commit | commitdiff | tree | snapshot
2011-03-16 Adam Megaczmajor overhaul of WeakToStrong/StrongToWeak; it can... commit | commitdiff | tree | snapshot
2011-03-16 Adam Megaczbetter variable names in HaskWeakToCore commit | commitdiff | tree | snapshot
2011-03-16 Adam Megaczrestrict RNote to one hypothesis, major additions to... commit | commitdiff | tree | snapshot
2011-03-16 Adam Megaczadd EGlobal/RGlobal for CoreVars whose binder we cannot see commit | commitdiff | tree | snapshot
2011-03-16 Adam Megaczadd crude Monad type class commit | commitdiff | tree | snapshot
2011-03-15 Adam Megaczfinal batch of fixups before enabling -fcoqpass commit | commitdiff | tree | snapshot
2011-03-15 Adam Megaczfix spellings in Extraction-prefix.hs, minor tweaks commit | commitdiff | tree | snapshot
2011-03-15 Adam Megaczformatting commit | commitdiff | tree | snapshot
2011-03-15 Adam Megaczchange names of Kind constructors to be more informative commit | commitdiff | tree | snapshot
2011-03-15 Adam Megaczreshuffle definitions in an attempt to iron out inter... commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczadd support for CSP in HaskCore+HaskWeak commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczremove dead code from HaskWeak commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczeliminate ext_tree_{left,right} keywords commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczmore formatting fixes commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczformatting fixes commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczminor cleanups, deleted dead code, eliminated use of... commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczfix sortAlts so it actually does something commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczadd tutorial.coqpass to gitignore commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczadd tutorial to the repository commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczrename weakTypeToType'' to weakTypeToTypeOfKind commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczrevise tyFunKind to use splitKind commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczadd splitKind to HaskKind commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczfix ToString instance for Kind commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczminor cleanups in HaskStrongToWeak commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczinclude URL for trfrac.sty and mathpartir in LaTeX... commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczfirst pass at proper handling of coercions in HaskWeak commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczbetter error reporting in HaskWeakToStrong commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczbetter error reporting in Extraction.v commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczclose numerous holes in HaskStrongToProof commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczmajor revision of HaskWeakToStrong, put phi/psi on... commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczfix spelling error in HaskWeakToCore commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczremove weakTypeOfWeakExpr and replaceWeakTypeVar, no... commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczstore the scrutinee CoreVar in WeakExpr Case to simplif... commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczstore the magic CoreVar for hetmet brak/esc in WeakExpr... commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczdetect (->) TyCon and substitute FunTy in WeakToCore commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczfix bugs in LaTeX output commit | commitdiff | tree | snapshot
2011-03-14 Adam MegaczToString instance for HaskCore commit | commitdiff | tree | snapshot
2011-03-14 Adam MegaczGeneral.addErrorMessage, orErrorBindWithMessage commit | commitdiff | tree | snapshot
2011-03-14 Adam Megaczmove eol:string to General.v commit | commitdiff | tree | snapshot
2011-03-13 Adam Megaczrestore HaskWeakToStrong functionality that I broke... commit | commitdiff | tree | snapshot
2011-03-13 Adam MegaczRemove unnecessary coreVar_eq_refl axiom commit | commitdiff | tree | snapshot
2011-03-13 Adam MegaczRename Extraction.fail to Extraction.Prelude_error commit | commitdiff | tree | snapshot
2011-03-13 Adam MegaczEliminate the need for WeakVar decidable equality axiom commit | commitdiff | tree | snapshot
2011-03-12 Adam Megaczupdate push-url in Makefile commit | commitdiff | tree | snapshot
2011-03-12 Adam MegaczMake the HaskStrong type representation Kind-indexed... commit | commitdiff | tree | snapshot
2011-03-09 Adam Megaczmore Makefile updates commit | commitdiff | tree | snapshot
2011-03-07 Adam MegaczMakefile updates commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczmake latex output use the preview package to set the... commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczadd HaskProofToStrong skeleton implementation commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczadd HaskStrongToWeak commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczadd HaskStrongToProof commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczadd HaskWeakToStrong commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczgive HaskWeak its own type representation, fix numerous... commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczbetter names for the auxiliary CaseBranch records commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczseparate type/coer/expr variables in HaskWeak case... commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczstore variables in ELetRecBindings rather than its... commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczadd HaskWeakToCore commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczadd proper proofs of the fact that every rule has exact... commit | commitdiff | tree | snapshot
2011-03-07 Adam MegaczChanged WEBrak/WEEsc to store a CoreType commit | commitdiff | tree | snapshot
2011-03-07 Adam MegaczAdded WeakVar, a separate variable representation for... commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczadded "publish" target to regenerate tex/pdf code commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczadded HaskCoreToWeak commit | commitdiff | tree | snapshot
2011-03-07 Adam Megaczcleaned up lots of FIXMEs in ProofToLatex commit | commitdiff | tree | snapshot
2011-03-02 Adam MegaczInitial checkin of Coq-in-GHC code commit | commitdiff | tree | snapshot
Coq proofs and code accompanying the HetMet extensions for GHC