projects / coq-hetmet.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
minor cleanups to Extraction-prefix.hs to eliminate warnings
[coq-hetmet.git] / src /
2011-05-09 Adam Megaczminor cleanups to Extraction-prefix.hs to eliminate... tree | commitdiff
2011-05-05 Adam Megaczfurther improvements to flattener tree | commitdiff
2011-05-03 Adam Megaczseparate HaskProofStratified into PCF.v, HaskProgrammin... tree | commitdiff
2011-04-30 Adam Megaczreorganize HaskProof files tree | commitdiff
2011-04-30 Adam Megaczclean up hints for NaturalDeduction, split ProgrammingL... tree | commitdiff
2011-04-29 Adam Megaczremove many [[admit]]s from HaskProofFlattener.v tree | commitdiff
2011-04-27 Adam MegaczMerge branch 'master' of git.megacz.com/coq-hetmet tree | commitdiff
2011-04-27 Adam Megaczprove all [admit]ted lemmas in HaskStrongToProof (not... tree | commitdiff
2011-04-25 Adam Megaczadd -fno-warn-unused-{binds,patterns} to Coq extraction tree | commitdiff
2011-04-25 Adam Megaczremove ClosedSIND (use "SIND []" instead) tree | commitdiff
2011-04-24 Adam Megaczremove all admits from ProgrammingLanguage.v tree | commitdiff
2011-04-24 Adam MegaczNaturalDeduction: add nd_swap, nd_prod_split, and some... tree | commitdiff
2011-04-18 Adam Megaczspeed up builds by removing some dependencies from... tree | commitdiff
2011-04-16 Adam Megaczfix erroneous conclusion to penultimate lemma tree | commitdiff
2011-04-11 Adam Megaczunbreak lots more stuff tree | commitdiff
2011-04-11 Adam Megaczuncomment some code in ProgrammingLanguage.v tree | commitdiff
2011-04-10 Adam Megaczremove the very last admit (missing proof) from General... tree | commitdiff
2011-04-10 Adam Megaczfix bug in GeneralizedArrowFromReification tree | commitdiff
2011-04-10 Adam MegaczAll.v: uncomment things tree | commitdiff
2011-04-10 Adam Megaczbugfix in ReificationsIsomorphicToGeneralizedArrows tree | commitdiff
2011-04-10 Adam Megaczadd commented-out definitions for analytic proofs and... tree | commitdiff
2011-04-10 Adam Megaczfill in lots of missing proofs tree | commitdiff
2011-04-10 Adam Megaczupdate to new coq-categories, base ND_Relation on inert... tree | commitdiff
2011-04-09 Adam Megaczremove notations from Preamble that come from coq-categ... tree | commitdiff
2011-04-04 Adam Megaczupdate to account for coq-categories changes tree | commitdiff
2011-04-02 Adam Megaczupdate submodule pointer, account for changes upstream tree | commitdiff
2011-04-02 Adam MegaczExtractionMain: better pdflatex code output tree | commitdiff
2011-04-02 Adam Megaczre-arrange ProgrammingLanguage tree | commitdiff
2011-04-02 Adam Megaczsplit HaskProofCategory into two files tree | commitdiff
2011-04-01 Adam Megaczremove unproven step1_lemma (it has a proof now) tree | commitdiff
2011-03-29 Adam Megaczformatting fixes tree | commitdiff
2011-03-29 Adam Megaczremove stale import from ExtractionMain tree | commitdiff
2011-03-29 Adam Megaczlots of cleanup tree | commitdiff
2011-03-29 Adam Megaczreorganize flattening code tree | commitdiff
2011-03-29 Adam MegaczHaskProofCategory: more work tree | commitdiff
2011-03-29 Adam Megaczswap the order of the hypotheses of RLet tree | commitdiff
2011-03-29 Adam MegaczNaturalDeduction: remove unnecessary scnd_leaf, add... tree | commitdiff
2011-03-28 Adam Megaczreplace UJudg with Arrange tree | commitdiff
2011-03-28 Adam Megaczcheckpoint tree | commitdiff
2011-03-28 Adam Megaczcheckpoint tree | commitdiff
2011-03-28 Adam Megaczfix typo tree | commitdiff
2011-03-28 Adam MegaczProgrammingLanguage: more implementation tree | commitdiff
2011-03-28 Adam MegaczHaskProofCategory: implement more tree | commitdiff
2011-03-28 Adam Megaczremove old code from WeakFunctorCategory tree | commitdiff
2011-03-28 Adam MegaczReificationsIsomorphicToGeneralizedArrows: use EqDep tree | commitdiff
2011-03-28 Adam MegaczNaturalDeduction: allow multi-rule implementations... tree | commitdiff
2011-03-28 Adam MegaczMerge branch 'master' of git.megacz.com/coq-hetmet tree | commitdiff
2011-03-28 Adam Megaczorganize Extraction-prefix.hs a bit tree | commitdiff
2011-03-28 Adam Megaczfallback plan: turn all CoreSyn coercions into unsafeCoerce tree | commitdiff
2011-03-27 Adam Megaczchange name of string-extraction placeholder tree | commitdiff
2011-03-27 Adam Megaczremove PreCategory tree | commitdiff
2011-03-27 Adam Megaczupdate submodule pointer tree | commitdiff
2011-03-27 Adam Megaczalmost finished with main theorem tree | commitdiff
2011-03-27 Adam Megaczcheckpoint tree | commitdiff
2011-03-27 Adam Megaczget rid of vec_{fst,snd} axioms tree | commitdiff
2011-03-27 Adam Megaczimprove error message tree | commitdiff
2011-03-27 Adam Megaczupdate submodule pointer tree | commitdiff
2011-03-27 Adam Megaczremove unnecessary comments tree | commitdiff
2011-03-27 Adam Megaczuse WeakFunctorCategory to prove GArrow/Reification... tree | commitdiff
2011-03-26 Adam Megacztemporarily comment out tree | commitdiff
2011-03-26 Adam Megaczmore bugfixes tree | commitdiff
2011-03-26 Adam Megaczfix {Reification,GeneralizedArrow}Category tree | commitdiff
2011-03-26 Adam Megaczimprovements to ProgrammingLanguage tree | commitdiff
2011-03-26 Adam MegaczProgrammingLanguage.v: add definitions for TypesL_... tree | commitdiff
2011-03-26 Adam Megaczfinish definitions for SequentCalculus, CutRule, Sequen... tree | commitdiff
2011-03-26 Adam Megacznote that REmptyGroup and RLit are flat tree | commitdiff
2011-03-26 Adam Megaczupdate submodule pointer tree | commitdiff
2011-03-26 Adam Megaczupdate submodule pointer tree | commitdiff
2011-03-26 Adam Megaczre-arrange NaturalDeduction tree | commitdiff
2011-03-26 Adam Megaczchange fst_zip/snd_zip to axioms tree | commitdiff
2011-03-26 Adam Megaczfix proof that Judgments(L) is Cartesian tree | commitdiff
2011-03-25 Adam Megaczadd Concatenable, LatexMath, and fix HaskProofToLatex tree | commitdiff
2011-03-25 Adam Megaczadd ToLatex instance for TyCon/TyFun tree | commitdiff
2011-03-25 Adam Megaczupdate categories submodule pointer tree | commitdiff
2011-03-25 Adam Megaczsplit Extraction.v so most can be compiled with -dont... tree | commitdiff
2011-03-25 Adam MegaczHaskProofToLatex improvements tree | commitdiff
2011-03-25 Adam MegaczHaskProofCategory: add commented-out-code tree | commitdiff
2011-03-25 Adam Megaczuse apply tactic in ReificationFromGeneralizedArrow... tree | commitdiff
2011-03-25 Adam MegaczProgrammingLanguage: significant cleanups tree | commitdiff
2011-03-25 Adam Megaczadd LetRec case to Rule_Flat tree | commitdiff
2011-03-25 Adam MegaczNaturalDeductionCategory: cleanup, add SequentCalculus... tree | commitdiff
2011-03-25 Adam Megaczadd ToLatex instance parameter to HaskStrong tree | commitdiff
2011-03-25 Adam Megaczremove unnecessary instance from HaskStrongTypes tree | commitdiff
2011-03-25 Adam Megaczchange import order in HaskWeakVars tree | commitdiff
2011-03-25 Adam Megaczchange import order in HaskCoreToWeak tree | commitdiff
2011-03-25 Adam Megaczadd n-ary form of nd_weak tree | commitdiff
2011-03-25 Adam Megaczadd ndr_void_proofs_irrelevant tree | commitdiff
2011-03-25 Adam Megaczmove ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons tree | commitdiff
2011-03-25 Adam Megaczadd kindToLatex in HaskKinds tree | commitdiff
2011-03-25 Adam Megaczadd ToLatex class, move machinery to General.v tree | commitdiff
2011-03-25 Adam Megaczadd machinery to create merged Coq script GArrow.v tree | commitdiff
2011-03-22 Adam Megaczupdate categories submodule pointer tree | commitdiff
2011-03-22 Adam Megaczproofs that Types/Judgments form an enrichment tree | commitdiff
2011-03-21 Adam Megaczadd distinctT, InT to General tree | commitdiff
2011-03-21 Adam Megaczadd HaskXXXXCategory, generalized arrows, and reifications tree | commitdiff
2011-03-21 Adam Megaczadd coq-categories as a submodule tree | commitdiff
2011-03-21 Adam Megaczmake StrongAlt a parameter rather than field in StrongC... tree | commitdiff
2011-03-20 Adam Megaczremove vec2list_injective tree | commitdiff
2011-03-20 Adam Megaczget rid of a bunch of admits in HaskStrongToProof tree | commitdiff
2011-03-20 Adam Megaczrequire all branches of LetRec be at the same level... tree | commitdiff
next
Coq proofs and code accompanying the HetMet extensions for GHC