aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
Commit message (Expand)AuthorAge
...
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
* Avoid using a deprecated lemma in the standard library.Gravatar Guillaume Melquiond2014-06-26
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* FinFun.v: results about injective/surjective/bijective fonctions over finite ...Gravatar Pierre Letouzey2014-02-07
* List: Bug 3039 weaker requirement for fold symmetricGravatar Pierre Boutillier2013-12-20
* Added a concat function to List theory. Strangely, it was missing.Gravatar ppedrot2013-07-24
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Updating headers.Gravatar herbelin2012-08-08
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* list_eq_dec now transparent (wish #2786)Gravatar letouzey2012-06-01
* SetoidList: explicit the fact that InfA_compat won't use ltA_strorderGravatar letouzey2012-05-22
* List + Permutation : more results about nth_error and nthGravatar letouzey2012-05-18
* A notion of permutation for lists modulo a setoid equalityGravatar letouzey2012-05-02
* Uniformisation in the documentation: remove the use of 'coinductive' inGravatar aspiwack2012-04-13
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Bug 2589: Documentation patch of Hendrik TewsGravatar pboutill2011-09-02
* A module out of Program to have list notations (bug 2463)Gravatar pboutill2011-04-08
* Simplify proofs in Permutation using generalized rewriting.Gravatar msozeau2011-03-04
* Remove obsolete TheoryListGravatar glondu2011-02-10
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Fixing definition of set_map (bug report #2111) which was actually alreadyGravatar herbelin2010-06-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Granting wish #2229 (InA_dec transparent) and Michael Day's coq-clubGravatar herbelin2010-04-10
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...Gravatar letouzey2009-11-02
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
* Fix flat_map definition so that it plays nicely with fixGravatar glondu2009-10-29
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Remove useless MonoList.vGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* adds a property on mapGravatar bertot2009-08-19
* adds lemmas on interactions between existsb, forallb, and appGravatar bertot2009-08-19
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 00:42:26 +0000