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
/
common
/
Separation.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Add `Declare Scope` where appropriate (#440)
Xavier Leroy
2022-09-19
1
-0
/
+1
*
Use the LGPL instead of the GPL for dual-licensed files
Xavier Leroy
2021-05-08
1
-4
/
+5
*
Do not depend on projection parameter names (#388)
Xia Li-yao
2021-03-25
1
-1
/
+1
*
Qualify `Hint` as `Global Hint` where appropriate
Xavier Leroy
2021-01-21
1
-1
/
+1
*
Replace `omega` tactic with `lia`
Xavier Leroy
2020-12-29
1
-33
/
+33
*
Coq 8.10 compatibility: make explicit the "core" hint database
Xavier Leroy
2019-08-05
1
-1
/
+1
*
lib/Coqlib.v: remove defns about multiplication, division, modulus
Xavier Leroy
2019-04-23
1
-1
/
+1
*
Remove coq warnings (#28)
Bernhard Schommer
2017-09-22
1
-4
/
+4
*
Hybrid 64bit/32bit PowerPC port
Bernhard Schommer
2017-05-03
1
-71
/
+71
*
Support for 64-bit architectures: generic support
Xavier Leroy
2016-10-01
1
-15
/
+15
*
Port to Coq 8.5pl2
Xavier Leroy
2016-07-08
1
-2
/
+1
*
Stricter control of permissions in memory injections and extensions
Xavier Leroy
2016-06-22
1
-0
/
+4
*
Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...
Xavier Leroy
2016-04-27
1
-0
/
+916