aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Decidableplus.v
Commit message (Expand)AuthorAgeFilesLines
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-21/+21
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-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