aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists/SetoidList.v
AgeCommit message (Expand)Author
2021-01-08Modify Lists/SetoidList.v to compile with -mangle-namesJasper Hugunin
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
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-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
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
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-07-10isolate instances about Permutation and PermutationA which may slow rewriteletouzey
2012-05-22SetoidList: explicit the fact that InfA_compat won't use ltA_strorderletouzey
2012-05-02A notion of permutation for lists modulo a setoid equalityletouzey
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-03-04Simplify proofs in Permutation using generalized rewriting.msozeau
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-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-10Granting wish #2229 (InA_dec transparent) and Michael Day's coq-clubherbelin
2009-11-02List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...letouzey
2009-10-19Merge SetoidList2 into SetoidList.letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-07-20Typo in a commentletouzey
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-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
2007-11-06small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is letouzey
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
2007-06-26additional properties for FMap (and slight rework of SetoidList and FSetPrope...letouzey
2007-06-14oups: one file forgotten in my previous commitletouzey
2007-06-08some more properties of fold and elements in FSetPropertiesletouzey
2006-05-23Changement de précédence de l'argument du by de assert; conséquences...herbelin
2006-05-22un debut de propriétés concernant FMapletouzey
2006-05-15petit ajout concernant InAletouzey
2006-05-11decidabilite de InA letouzey
2006-05-11Duplication du fichier FSetProperties pour les ensembles Weak. letouzey
2006-04-06versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesletouzey
2006-03-16propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d...letouzey
2006-03-16utilisation de removeA dans FSetPropertiesletouzey
2006-03-15renommage NoRedun vers le plus joli NoDupletouzey
2006-03-15Typoletouzey
2006-03-15Ajout de fonctions sur les listesnotin
2006-03-15Ajout de theories/FSets contenant la partie "light" de FSets et FMap:letouzey