aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists
AgeCommit message (Expand)Author
2010-02-17Arith's min and max placed in Peano (+basic specs max_l and co)letouzey
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-11-02List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...letouzey
2009-11-02Remove various useless {struct} annotationsletouzey
2009-11-02list, length, app are migrated from List to Datatypesletouzey
2009-10-29Fix flat_map definition so that it plays nicely with fixglondu
2009-10-19Merge SetoidList2 into SetoidList.letouzey
2009-10-13MSets: a new generation of FSetsletouzey
2009-10-08Implicit argument of Logic.eq become maximally insertedletouzey
2009-09-17Remove useless MonoList.vglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-19adds a property on mapbertot
2009-08-19adds lemmas on interactions between existsb, forallb, and appbertot
2009-08-04- Add more precise error localisation when one of the application failsherbelin
2009-07-24List: add a iff-based lemma about In and ++letouzey
2009-07-20Typo in a commentletouzey
2009-06-06Very-small-step policy changes to the library.herbelin
2009-03-18fixed ring/field warning about hyp cleaning upbarras
2009-03-17- gros commit sur ring et field: passage des arguments simplifiebarras
2009-01-18Various little fixes:msozeau
2008-12-26FMaps: various updates (mostly suggested by P. Casteran)letouzey
2008-12-22FMap: fold_rec + more permissive transpose hyp + various cleanupletouzey
2008-08-06Add lemmas on lists: nth_default_eq, map_nth_errorglondu
2008-05-27Cyclic31: migrate auxiliary lemmas to their legitimate filesletouzey
2008-05-09Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]herbelin
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey
2008-04-29Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laherbelin
2008-04-28Backtrack on using metas eagerly in auto, only done in "new auto" formsozeau
2008-04-27- Fix bug in unification not taking into account the right metamsozeau
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-04-01Correction du bug #1819notin
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-11-06small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is letouzey
2007-11-01two additionnal results on list append (coming from theories/ints/List/ListAu...letouzey
2007-07-11Added ForAll_Str_nth_tlroconnor
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
2007-06-26Added zwqipWith.roconnor
2007-06-26additional properties for FMap (and slight rework of SetoidList and FSetPrope...letouzey
2007-06-14oups: one file forgotten in my previous commitletouzey
2007-06-08some more properties of fold and elements in FSetPropertiesletouzey
2007-04-17Correction du bug #1510notin
2007-04-13Correction bug #1499notin
2006-12-11Changement dans le kernel : bgregoir
2006-10-26Déplacement des propriétés générales de BinList dans List et des tactiqu...herbelin
2006-09-01Indentation + typonotin
2006-07-09Argument Scope de list déplacé dans List.vherbelin
2006-07-06Quelques Hint inutilesherbelin