aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/abstractbb
Commit message (Expand)AuthorAgeFilesLines
* 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
* remove cumbersome dependency on genv in bblock_eq_testSylvain Boulmé2019-03-053-27/+27
* (Unsafe) coercion of ??bool into boolSylvain Boulmé2019-03-021-2/+2
* [BROKEN] trying to generalize Sylvain's abstract bb to include a genv.Cyril SIX2019-02-207-87/+133
* Added AbstractBasicBlock files to the Coq build processCyril SIX2019-02-1325-0/+4692