aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-profilingDavid Monniaux2020-04-083-157/+152
|\
| * Some cleaning on Linearize and DuplicateCyril SIX2020-04-082-95/+118
| * Duplicate: Common rtl_successors functionCyril SIX2020-04-081-61/+33
| * accept Coq 8.11.1David Monniaux2020-04-081-1/+1
* | fixDavid Monniaux2020-04-081-3/+3
* | rm commented-out stuffDavid Monniaux2020-04-081-86/+0
* | last QedDavid Monniaux2020-04-081-5/+139
* | progress in proofsDavid Monniaux2020-04-081-1/+71
* | progress in proofsDavid Monniaux2020-04-081-0/+66
* | progress in proofsDavid Monniaux2020-04-081-0/+90
* | progress in proofsDavid Monniaux2020-04-081-4/+9
* | progress in proofsDavid Monniaux2020-04-081-3/+21
* | progress in proofsDavid Monniaux2020-04-081-2/+8
* | progress in proofsDavid Monniaux2020-04-081-1/+6
* | progress in proofsDavid Monniaux2020-04-081-3/+23
* | progress in proofsDavid Monniaux2020-04-081-3/+25
* | progress in proofsDavid Monniaux2020-04-081-0/+24
* | progress in proofsDavid Monniaux2020-04-081-16/+25
* | progress in proofsDavid Monniaux2020-04-081-1/+78
* | -fbranch-probabilitiesDavid Monniaux2020-04-081-1/+2
* | reloading and exploiting seems to workDavid Monniaux2020-04-088-15/+72
* | fixed a bug in support libraries; reload profiling infoDavid Monniaux2020-04-085-8/+42
* | library support for writing profiling information to filesDavid Monniaux2020-04-083-4/+65
* | print profiling idsDavid Monniaux2020-04-081-3/+23
* | looks like it works?David Monniaux2020-04-082-4/+39
* | print hashesDavid Monniaux2020-04-086-13/+28
* | so that it gets printedDavid Monniaux2020-04-081-0/+3
* | installed Profiling (not finished)David Monniaux2020-04-085-25/+273
* | begin installing profilingDavid Monniaux2020-04-0810-54/+73
* | begin profiling stuffDavid Monniaux2020-04-081-0/+57
* | added EF_profilingDavid Monniaux2020-04-087-15/+77
|/
* Changing best_predecessor_of to not take None predictionsCyril SIX2020-04-031-4/+15
* Fixing loop heuristicCyril SIX2020-04-021-15/+34
* Stopping traces at join pointsCyril SIX2020-04-011-2/+25
* Merge remote-tracking branch 'origin/mppa-work' into mppa-branch-infoCyril SIX2020-04-0136-477/+2024
|\
| * Fixing packedstruct issuev3.7_mppa_2020-04-01Cyril SIX2020-04-012-15/+15
| * Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-0112-80/+926
| |\
| | * Updates for release 3.7v3.7Xavier Leroy2020-03-311-1/+1
| | * Updates for release 3.7Xavier Leroy2020-03-312-1/+6
| | * Update ChangelogXavier Leroy2020-03-311-3/+34
| | * Double rounding error in int64->float32 conversions on PowerPC and ARMXavier Leroy2020-03-304-24/+22
| | * Add a test for int64 -> float32 conversionXavier Leroy2020-03-302-39/+838
| | * Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-293-12/+25
| * | -fduplicate -1 really desactivates the pass in Coq nowCyril SIX2020-04-013-7/+8
| * | Fix cutrewrite deprecatedCyril SIX2020-04-011-3/+4
| * | Removing 8.8.* versions of coq in configureCyril SIX2020-04-011-1/+1
| * | do not run check-admitted alwaysDavid Monniaux2020-03-311-0/+8
| * | move check-admitted elsewhereDavid Monniaux2020-03-311-2/+6
| * | forgot imageDavid Monniaux2020-03-311-0/+1
| * | add check-admittedDavid Monniaux2020-03-311-0/+6