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
/
exportclight
/
Clightdefs.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Use the LGPL instead of the GPL for dual-licensed files
Xavier Leroy
2021-05-08
1
-4
/
+5
*
Move `$` notation in submodule `ClightNotations` and scope `clight_scope`
Xavier Leroy
2021-04-23
1
-11
/
+23
*
Add `string_of_ident` conversion
Xavier Leroy
2020-10-12
1
-0
/
+110
*
Add a canonical encoding of identifiers as numbers and use it in clightgen (#...
Xavier Leroy
2020-05-19
1
-1
/
+100
*
Issue #199: improve namespace management for clightgen-produced files
Xavier Leroy
2017-08-28
1
-11
/
+2
*
Issue #196: excessive proof-checking times in .v files generated by clightgen
Xavier Leroy
2017-08-15
1
-5
/
+24
*
Use Coq strings instead of idents to name external and builtin functions.
Xavier Leroy
2015-10-11
1
-0
/
+1
*
Update clightgen with respect to new representation of composites.
Xavier Leroy
2015-02-20
1
-3
/
+10
*
Update clightgen for CompCert 2.2.
v2.2
xleroy
2014-02-23
1
-1
/
+1
*
Merge of the "alignas" branch.
xleroy
2013-10-05
1
-10
/
+18
*
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
xleroy
2013-04-20
1
-0
/
+3
*
Put clighgen files in exportclight/
xleroy
2013-01-05
1
-0
/
+53