index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
lib
/
Parmov.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge pull request #191 from sigurdschneider/master
Xavier Leroy
2017-10-20
1
-1
/
+1
|
\
|
*
Ensure FunInd or Recdef is imported if functional induction is used
Sigurd Schneider
2017-07-20
1
-1
/
+1
*
|
Remove coq warnings (#28)
Bernhard Schommer
2017-09-22
1
-1
/
+1
|
/
*
Updated PR by removing whitespaces. Bug 17450.
Bernhard Schommer
2015-10-20
1
-154
/
+154
*
Silence the warning "Cannot build inversion information".
xleroy
2014-02-24
1
-9
/
+10
*
Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.
xleroy
2011-03-09
1
-1
/
+1
*
Merging the Princeton implementation of the memory model. Separate axioms in...
xleroy
2010-06-28
1
-3
/
+4
*
Adapted to work with Coq 8.2-1
v1.4.1
xleroy
2009-06-05
1
-4
/
+4
*
Ajout license, README, copyright notices
xleroy
2008-01-27
1
-0
/
+17
*
Function -> Definition (probleme de performance avec Coq8.1pl3)
xleroy
2008-01-07
1
-1
/
+1
*
Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...
xleroy
2007-12-08
1
-6
/
+363
*
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
xleroy
2007-08-04
1
-229
/
+276
*
Fusion de la branche "traces":
xleroy
2006-09-04
1
-0
/
+1206