aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sorting/Permutation.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar 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
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
* Updating headers.Gravatar herbelin2012-08-08
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
* Permutation: remove a compatibility notation which doesn't help MathClassesGravatar letouzey2012-05-22
* List + Permutation : more results about nth_error and nthGravatar letouzey2012-05-18
* Simplify proofs in Permutation using generalized rewriting.Gravatar msozeau2011-03-04
* In passing, very quick uniformization of coqdoc headers in a few files.Gravatar herbelin2010-12-09
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Sorting library: export as hints only lemmas that obviously simplifyGravatar herbelin2010-07-02
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13
* Sorting/Permutation: no need to require the whole Arith (and hence plugins li...Gravatar letouzey2009-11-02
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Coq.Relations.Relations can move back to its short nameGravatar letouzey2008-03-19
* Suppress some warnings by writing ugly Coq.Relations.Relations in some .vGravatar letouzey2008-03-14
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* Mise en forme des theoriesGravatar notin2006-10-17
* etoffage des notions de permutations (a la fois List.Permutation et Permutati...Gravatar letouzey2006-05-16
* quelques ajouts venant des fichiers de Evelyne C. Gravatar letouzey2006-05-11
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* remise au gout du jour du repertoire theories/Sorting de la V6.3Gravatar letouzey2001-11-21