aboutsummaryrefslogtreecommitdiffstats
path: root/common/Separation.v
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-5/+6
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-1/+1
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-33/+33
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-1/+1
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-1/+1
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-4/+4
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-71/+71
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-15/+15
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-2/+1
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-221-0/+4
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-0/+916