aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Parmov.v
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-1/+1
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-1/+1
* | Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
|/
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-154/+154
* Silence the warning "Cannot build inversion information".xleroy2014-02-241-9/+10
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-1/+1
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-3/+4
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-4/+4
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+17
* Function -> Definition (probleme de performance avec Coq8.1pl3)xleroy2008-01-071-1/+1
* Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...xleroy2007-12-081-6/+363
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-229/+276
* Fusion de la branche "traces":xleroy2006-09-041-0/+1206