aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/abstractbb/Impure/ImpPrelude.v
Commit message (Expand)AuthorAgeFilesLines
* abstractbb: support of removing useless computationsSylvain Boulmé2019-05-141-1/+28
* moving iandb from ImpCore to ImpPreludeSylvain Boulmé2019-04-081-15/+17
* Impure: improved iandb + struct_eqSylvain Boulmé2019-04-011-2/+2
* Fix for CompCert 3.5Cyril SIX2019-03-131-0/+1
* quick fix of equalities issuesSylvain Boulmé2019-03-051-0/+4
* Added AbstractBasicBlock files to the Coq build processCyril SIX2019-02-131-0/+163