aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/abstractbb/Impure
Commit message (Expand)AuthorAgeFilesLines
* generalize bblock_equiv into bblock_simu (abstract_bb)Sylvain Boulmé2019-05-071-12/+3
* update from Impure LibrarySylvain Boulmé2019-04-111-20/+22
* moving iandb from ImpCore to ImpPreludeSylvain Boulmé2019-04-082-23/+18
* Impure: improved iandb + struct_eqSylvain Boulmé2019-04-012-3/+11
* Fix for CompCert 3.5Cyril SIX2019-03-131-0/+1
* quick fix of equalities issuesSylvain Boulmé2019-03-051-0/+4
* fix extraction of ImpConfigSylvain Boulmé2019-03-051-2/+5
* compilation of ImpIOOraclesSylvain Boulmé2019-03-052-4/+8
* (Unsafe) coercion of ??bool into boolSylvain Boulmé2019-03-021-2/+2
* Added AbstractBasicBlock files to the Coq build processCyril SIX2019-02-1316-0/+1431