summaryrefslogtreecommitdiff
path: root/lib/Lattice.v
Commit message (Expand)AuthorAge
* Merge of branch value-analysis.Gravatar xleroy2013-12-20
* Simplify LPMap by smashing bottoms.Gravatar xleroy2013-08-12
* Update LICENSE file and headers for dual-licensed files.Gravatar xleroy2013-06-17
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
* Maps: revised TREE interface; added mucho derived properties and operations i...Gravatar xleroy2013-03-12
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in Gravatar xleroy2013-03-09
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.Gravatar xleroy2011-03-09
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...Gravatar xleroy2010-10-27
* Coloringaux: make identifiers unique; special treatment of precolored Gravatar xleroy2009-08-26
* Cil2Csyntax: added goto and labels; added assignment between structsGravatar xleroy2009-08-16
* Adapted to work with Coq 8.2-1Gravatar xleroy2009-06-05
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* CommentairesGravatar xleroy2007-03-05
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...Gravatar xleroy2007-03-02
* Initial import of compcertGravatar xleroy2006-02-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 18:28:53 +0000