aboutsummaryrefslogtreecommitdiff
path: root/checker/inductive.ml
AgeCommit message (Expand)Author
2012-03-02Noise for nothingpboutill
2010-09-24Checker: remove some dead codeletouzey
2010-07-30adpated the checker to handle coomutative cuts and lazynessbarras
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2009-10-21This big commit addresses two problems:soubiran
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-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-04-21added the .vo checker (with independent Makefile)barras