Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Adding copyrights | Cyril SIX | 2020-05-04 | 4 | -0/+48 |
* | moved to extra | David Monniaux | 2020-04-16 | 1 | -0/+0 |
* | gmap2_idem | David Monniaux | 2020-04-16 | 1 | -65/+111 |
* | gmap2_idem | David Monniaux | 2020-04-16 | 1 | -0/+16 |
* | gmap2_idem_Empty | David Monniaux | 2020-04-16 | 1 | -0/+54 |
* | begin HashedMaps | David Monniaux | 2020-04-16 | 1 | -0/+332 |
* | forward_move_l | David Monniaux | 2020-03-10 | 1 | -1/+13 |
* | kill_reg_sound | David Monniaux | 2020-03-09 | 1 | -1/+1 |
* | CSE3 generate lists of killable | David Monniaux | 2020-03-05 | 1 | -0/+4 |
* | more about extraction and linking | David Monniaux | 2020-03-05 | 1 | -185/+180 |
* | streamlined lattice code | David Monniaux | 2020-03-05 | 2 | -30/+15 |
* | HashedSet with extraction | David Monniaux | 2020-03-05 | 1 | -0/+6 |
* | HashedSet with module types | David Monniaux | 2020-03-05 | 1 | -0/+115 |
* | move lattice stuff where it belongs | David Monniaux | 2020-03-05 | 4 | -0/+1446 |
* | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2020-03-03 | 3 | -96/+317 |
|\ | |||||
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2020-02-08 | 1 | -4/+5 |
| |\ | |||||
| * \ | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-01-15 | 1 | -1/+178 |
| |\ \ | |||||
| | * | | shrx'1_shr' | David Monniaux | 2020-01-14 | 1 | -1/+127 |
| | * | | shrx1_shr | David Monniaux | 2020-01-14 | 1 | -0/+51 |
| * | | | set_disjoint | David Monniaux | 2019-12-13 | 1 | -0/+49 |
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-11-13 | 4 | -12/+15 |
| |\| | | |||||
| * | | | [regression to check!] Merge tag 'v3.6' into mppa-work | Cyril SIX | 2019-10-16 | 2 | -65/+517 |
| |\ \ \ | |||||
| * | | | | Icond | Cyril SIX | 2019-10-07 | 1 | -0/+5 |
| * | | | | Ibuiltin proof | Cyril SIX | 2019-10-04 | 2 | -12/+89 |
| * | | | | Adding decidable equality for int | Cyril SIX | 2019-10-04 | 1 | -1/+12 |
| * | | | | Coq 8.10 compatibility: tweak Argument command | Xavier Leroy | 2019-08-05 | 1 | -1/+1 |
| * | | | | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-05 | 1 | -2/+2 |
* | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2 | David Monniaux | 2020-02-27 | 1 | -4/+5 |
|\ \ \ \ \ | | |_|_|/ | |/| | | | |||||
| * | | | | Reduce the checking time for the "decidable_equality_from" tactic | xavier.leroy | 2020-01-30 | 1 | -4/+5 |
| | |_|/ | |/| | | |||||
* | | | | progress on wellformed reg | David Monniaux | 2020-02-05 | 1 | -1/+120 |
* | | | | gremove_t | David Monniaux | 2020-02-04 | 1 | -0/+36 |
* | | | | gcombine_null | David Monniaux | 2020-02-04 | 1 | -0/+13 |
* | | | | gcombine_null | David Monniaux | 2020-02-04 | 1 | -1/+39 |
|/ / / | |||||
* | | | Use `intuition idtac` instead of `intuition` (#321) | Vincent Laporte | 2019-11-12 | 1 | -1/+1 |
* | | | More robust proof of `size_and` (#320) | Frédéric Besson | 2019-10-30 | 1 | -4/+5 |
* | | | Make explicit the use of hints from OrderedType (#316) | Vincent Laporte | 2019-10-02 | 2 | -7/+9 |
| |/ |/| | |||||
* | | AArch64 port | Xavier Leroy | 2019-08-08 | 1 | -24/+136 |
* | | More lemmas about powers of 2 | Xavier Leroy | 2019-08-07 | 1 | -0/+14 |
* | | Added Int.same_if_eq | Xavier Leroy | 2019-08-07 | 1 | -0/+5 |
* | | Properties of combinations of shifts and zero-/sign-extension | Xavier Leroy | 2019-08-07 | 1 | -0/+249 |
* | | Define integer sign extension for zero bits | Xavier Leroy | 2019-08-07 | 2 | -42/+57 |
* | | Zbits.v: add bit extraction and bit insertion | Xavier Leroy | 2019-08-07 | 1 | -0/+57 |
* | | Coq 8.10 compatibility: tweak Argument command | Xavier Leroy | 2019-08-07 | 1 | -1/+1 |
* | | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-07 | 1 | -2/+2 |
|/ | |||||
* | Another way to derive floatofintu from floatofint | Xavier Leroy | 2019-07-17 | 1 | -0/+41 |
* | Add floating-point square root and fused multiply-add | Xavier Leroy | 2019-07-17 | 1 | -3/+51 |
* | Revised specification of NaN payload behavior | Xavier Leroy | 2019-07-12 | 1 | -124/+104 |
* | New parser based on new version of the Coq backend of Menhir (#276) | Jacques-Henri Jourdan | 2019-07-05 | 1 | -51/+0 |
* | Avoid relying on `Export` bug (#301) | Maxime Dénès | 2019-07-04 | 1 | -1/+2 |
* | More efficient test for powers of two | Xavier Leroy | 2019-05-09 | 2 | -26/+105 |