summaryrefslogtreecommitdiff
path: root/lib/Iteration.v
Commit message (Expand)AuthorAge
* Update LICENSE file and headers for dual-licensed files.Gravatar xleroy2013-06-17
* Glasnost: making transparent a number of definitions that were opaqueGravatar xleroy2013-03-10
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* Merge of the newmem branch:Gravatar xleroy2012-05-21
* Merging the Princeton implementation of the memory model. Separate axioms in...Gravatar xleroy2010-06-28
* Adapted to work with Coq 8.2-1Gravatar xleroy2009-06-05
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
* Utilisation de FunctionGravatar xleroy2007-03-23
* Fusion de la branche "traces":Gravatar xleroy2006-09-04