summaryrefslogtreecommitdiff
path: root/lib/Maps.v
Commit message (Expand)AuthorAge
* Bind some local defs with Let, makes extracted code cleanerGravatar xleroy2013-03-12
* Maps: revised TREE interface; added mucho derived properties and operations i...Gravatar xleroy2013-03-12
* Useless ImportGravatar xleroy2013-03-10
* Glasnost: making transparent a number of definitions that were opaqueGravatar xleroy2013-03-10
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in Gravatar xleroy2013-03-09
* Memdata: cleanup continuedGravatar xleroy2012-05-26
* Merge of the newmem branch:Gravatar xleroy2012-05-21
* Cleaned up old commented-out partsGravatar xleroy2011-08-19
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...Gravatar xleroy2010-10-27
* Merge of the newmem and newextcalls branches:Gravatar xleroy2010-03-07
* Coloringaux: make identifiers unique; special treatment of precolored Gravatar xleroy2009-08-26
* Cil2Csyntax: added goto and labels; added assignment between structsGravatar xleroy2009-08-16
* Added 'going wrong' behaviorsGravatar xleroy2009-08-05
* Adapted to work with Coq 8.2-1Gravatar xleroy2009-06-05
* Suppression de 'exten', inutiliseGravatar xleroy2008-05-30
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...Gravatar xleroy2007-03-02
* Ajout operation eq dans PMap et IndexedMapGravatar xleroy2007-01-03
* Initial import of compcertGravatar xleroy2006-02-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 06:15:16 +0000