aboutsummaryrefslogtreecommitdiff
path: root/checker/reduction.ml
AgeCommit message (Expand)Author
2012-10-06still some more dead code removalletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-08-08Updating headers.herbelin
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-02Noise for nothingpboutill
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-03-04checker: cleanupglondu
2011-03-04checker: add eta-expansionglondu
2010-09-24Checker: remove some dead codeletouzey
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
2010-07-30adpated the checker to handle coomutative cuts and lazynessbarras
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29After the approval of Bruno, here the patch for the checker.soubiran
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-22Transfers to checker ("let"s in inductive arities + Coq root read-only).herbelin
2008-09-02[checker] basic conversion oracle: expand local vars firstbarras
2008-05-20also fixed conversion of the checkerbarras
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-04-21added the .vo checker (with independent Makefile)barras