summaryrefslogtreecommitdiff
path: root/lib/Parmov.v
Commit message (Expand)AuthorAge
* Silence the warning "Cannot build inversion information".Gravatar xleroy2014-02-24
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.Gravatar xleroy2011-03-09
* 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
* Function -> Definition (probleme de performance avec Coq8.1pl3)Gravatar xleroy2008-01-07
* Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...Gravatar xleroy2007-12-08
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
* Fusion de la branche "traces":Gravatar xleroy2006-09-04