aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists/List.v
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-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-13MSets: a new generation of FSetsletouzey
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-06-06Very-small-step policy changes to the library.herbelin
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-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
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
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
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
2006-05-17Typo dans List.vnotin
2006-05-17Ajout de [count_occ] dans List.vnotin
2006-05-16etoffage des notions de permutations (a la fois List.Permutation et Permutati...letouzey
2006-05-14In_dec de nouveau transparentletouzey
2006-05-11 r9089@thot: notin | 2006-05-10 14:40:51 +0200notin
2006-04-06versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesletouzey
2006-03-17Modification des propriétés (svn:executable)notin
2004-12-19In_dec transparent (wish #902)herbelin
2004-07-16Nouvelle en-têteherbelin
2003-12-24Ajout delimiteur et arguments de scope pour listherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2002-02-14option -dump-glob pour coqdocfilliatr
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19Mise de (*i autour CVS infomohring
2001-03-15entetesfilliatr
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-06-21theories/Listsfilliatr