aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists/SetoidList.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* 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
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* - 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
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
* SetoidList: explicit the fact that InfA_compat won't use ltA_strorderGravatar letouzey2012-05-22
* A notion of permutation for lists modulo a setoid equalityGravatar letouzey2012-05-02
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Simplify proofs in Permutation using generalized rewriting.Gravatar msozeau2011-03-04
* 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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Granting wish #2229 (InA_dec transparent) and Michael Day's coq-clubGravatar herbelin2010-04-10
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...Gravatar letouzey2009-11-02
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Typo in a commentGravatar letouzey2009-07-20
* Various little fixes:Gravatar msozeau2009-01-18
* FMaps: various updates (mostly suggested by P. Casteran)Gravatar letouzey2008-12-26
* FMap: fold_rec + more permissive transpose hyp + various cleanupGravatar letouzey2008-12-22
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* - Extensions of FMap(Weak)Facts: Gravatar letouzey2007-06-27
* additional properties for FMap (and slight rework of SetoidList and FSetPrope...Gravatar letouzey2007-06-26
* oups: one file forgotten in my previous commitGravatar letouzey2007-06-14
* some more properties of fold and elements in FSetPropertiesGravatar letouzey2007-06-08
* Changement de précédence de l'argument du by de assert; conséquences...Gravatar herbelin2006-05-23
* un debut de propriétés concernant FMapGravatar letouzey2006-05-22
* petit ajout concernant InAGravatar letouzey2006-05-15
* decidabilite de InA Gravatar letouzey2006-05-11
* Duplication du fichier FSetProperties pour les ensembles Weak. Gravatar letouzey2006-05-11
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
* propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d...Gravatar letouzey2006-03-16
* utilisation de removeA dans FSetPropertiesGravatar letouzey2006-03-16
* renommage NoRedun vers le plus joli NoDupGravatar letouzey2006-03-15
* TypoGravatar letouzey2006-03-15
* Ajout de fonctions sur les listesGravatar notin2006-03-15
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 22:15:04 +0000