aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Decidableplus.v
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-3/+3
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-2/+2
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-14/+14
* Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-0/+28
* Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 libraryXavier Leroy2016-09-171-48/+1
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-0/+244