index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
common
/
Smallstep.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Put forward_simulation and backward_simulation in Prop instead of Type
Xavier Leroy
2016-03-06
1
-255
/
+275
*
Updated PR by removing whitespaces. Bug 17450.
Bernhard Schommer
2015-10-20
1
-175
/
+175
*
Make small-step semantics more parametric w.r.t. the type of global environme...
Xavier Leroy
2014-11-26
1
-22
/
+37
*
Add Genv.public_symbol operation.
Xavier Leroy
2014-11-24
1
-14
/
+14
*
Remove some useless "Require".
xleroy
2012-12-30
1
-1
/
+0
*
Merge of the "volatile" branch:
xleroy
2012-02-04
1
-28
/
+275
*
Merge of branch new-semantics: revised and strengthened top-level statements ...
xleroy
2011-07-15
1
-457
/
+994
*
Merge of branches/full-expr-4:
xleroy
2010-08-18
1
-0
/
+50
*
Existence of behaviors
xleroy
2010-01-31
1
-2
/
+126
*
Distinguish two kinds of nonterminating behaviors: silent divergence
xleroy
2009-08-16
1
-25
/
+262
*
Added 'going wrong' behaviors
xleroy
2009-08-05
1
-11
/
+34
*
Adapted to work with Coq 8.2-1
v1.4.1
xleroy
2009-06-05
1
-8
/
+8
*
Fusion partielle de la branche contsem:
xleroy
2008-07-08
1
-54
/
+123
*
Ajout license, README, copyright notices
xleroy
2008-01-27
1
-0
/
+15
*
Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...
xleroy
2007-08-28
1
-13
/
+18
*
Ajout de common/Complements.v
xleroy
2007-08-26
1
-0
/
+10
*
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
xleroy
2007-08-04
1
-0
/
+460