aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists
AgeCommit message (Expand)Author
2012-06-01list_eq_dec now transparent (wish #2786)letouzey
2012-05-22SetoidList: explicit the fact that InfA_compat won't use ltA_strorderletouzey
2012-05-18List + Permutation : more results about nth_error and nthletouzey
2012-05-02A notion of permutation for lists modulo a setoid equalityletouzey
2012-04-13Uniformisation in the documentation: remove the use of 'coinductive' inaspiwack
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
2011-04-08A module out of Program to have list notations (bug 2463)pboutill
2011-03-04Simplify proofs in Permutation using generalized rewriting.msozeau
2011-02-10Remove obsolete TheoryListglondu
2010-12-17Cosmetic : let's take advantage of the n-ary exists notationletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-06-13Fixing definition of set_map (bug report #2111) which was actually alreadyherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-10Granting wish #2229 (InA_dec transparent) and Michael Day's coq-clubherbelin
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