aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists
AgeCommit message (Expand)Author
2014-12-28Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...Arnaud Spiwack
2014-12-18Adds two lemmas about hderror to the List standard library.Sébastien Hinderer
2014-12-18Implement the nodup function on lists and prove associated results.Sébastien Hinderer
2014-12-18Lists: enhanced version of Seb's last commit on Exists/ForallPierre Letouzey
2014-12-18Lists: a few results on Exists and Forall and a bit of code cleanup.Sébastien Hinderer
2014-12-11List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Pierre Letouzey
2014-12-11First series of results on lists.Sébastien Hinderer
2014-11-18Clarifying the role of ListSet.v in the library, compared to otherHugo Herbelin
2014-08-05Improving printing of "[]" (nil) in spite of the risk of collisionHugo Herbelin
2014-08-05Testing a replacement of "cut" by "enough" on a couple of test files.Hugo Herbelin
2014-08-05More proofs independent of the names generated by induction/elim overHugo Herbelin
2014-07-31Adding a generalized version of fold_Equal to FMapFacts.Pierre Courtieu
2014-06-26Avoid using a deprecated lemma in the standard library.Guillaume Melquiond
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-07FinFun.v: results about injective/surjective/bijective fonctions over finite ...Pierre Letouzey
2013-12-20List: Bug 3039 weaker requirement for fold symmetricPierre Boutillier
2013-07-24Added a concat function to List theory. Strangely, it was missing.ppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-08-08Updating headers.herbelin
2012-07-10isolate instances about Permutation and PermutationA which may slow rewriteletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-29 18:34:57 +0000