aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/Recdef.v
AgeCommit message (Expand)Author
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Recdef do now a Require Export FunInd (better compat)Pierre Letouzey
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2013-11-21Add Acc_intro_generator on top of all wf function proof (much much faster exe...Julien Forest
2012-08-08Updating headers.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey