rename constructors of Arrange to start with A instead of R
[coq-hetmet.git] / src / ExtractionMain.v
2011-05-28 Adam Megaczrename constructors of Arrange to start with A instead...
2011-05-28 Adam Megaczmove Arrange into NaturalDeductionContext
2011-05-28 Adam Megaczmigrate HaskStrong away from using LeveledHaskType
2011-05-27 Adam MegaczHaskProof: make the succedent level part of the judgment
2011-05-26 Adam Megaczadd new Where rule, eliminate unnecessary ga_swaps...
2011-05-14 Adam Megaczintegrate skolemization pass with flattening
2011-05-12 Adam Megaczswap order of hypotheses in RApp to match RLet
2011-05-10 Adam Megaczstart using type-family-based GArrow classes
2011-05-09 Adam Megaczsplit HaskLiteralsAndTyCons into two files
2011-05-09 Adam Megaczadd support for hetmet_unflatten
2011-05-09 Adam Megaczadd support for hetmet_flatten casting variable
2011-05-09 Adam Megaczallow -fcoqpass to change the type of top-level bindings
2011-05-09 Adam Megaczabstract out the kind of environment classifiers (ECKind)
2011-05-09 Adam Megaczmajor improvements to flattener; almost finished now
2011-05-05 Adam Megaczfurther improvements to flattener
2011-04-30 Adam Megaczreorganize HaskProof files
2011-04-18 Adam Megaczspeed up builds by removing some dependencies from...
2011-04-10 Adam Megaczfill in lots of missing proofs
2011-04-04 Adam Megaczupdate to account for coq-categories changes
2011-04-02 Adam MegaczExtractionMain: better pdflatex code output
2011-04-02 Adam Megaczsplit HaskProofCategory into two files
2011-03-29 Adam Megaczremove stale import from ExtractionMain
2011-03-29 Adam Megaczlots of cleanup
2011-03-29 Adam Megaczreorganize flattening code
2011-03-28 Adam Megaczreplace UJudg with Arrange
2011-03-27 Adam Megaczchange name of string-extraction placeholder
2011-03-27 Adam Megaczcheckpoint
2011-03-27 Adam Megaczimprove error message
2011-03-26 Adam Megaczre-arrange NaturalDeduction
2011-03-25 Adam Megaczadd Concatenable, LatexMath, and fix HaskProofToLatex
2011-03-25 Adam Megaczsplit Extraction.v so most can be compiled with -dont...