Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | coq 8.13.2 | David Monniaux | 2021-06-07 | 1 | -2/+1 |
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend... | Cyril SIX | 2021-06-01 | 31 | -144/+155 |
* | replacing omega with lia in some file | Léo Gourdin | 2021-03-29 | 2 | -32/+34 |
* | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 15 | -1150/+1176 |
|\ | |||||
| * | Qualify `Hint` as `Global Hint` where appropriate | Xavier Leroy | 2021-01-21 | 3 | -33/+36 |
| * | Define `fold_ind_aux` and `fold_ind` transparently | Xavier Leroy | 2021-01-21 | 1 | -2/+2 |
| * | Add new fold_ind induction principle for folds | Xavier Leroy | 2021-01-13 | 1 | -63/+82 |
| * | Add lemma list_norepet_rev | Xavier Leroy | 2021-01-13 | 1 | -0/+8 |
| * | Replace `omega` tactic with `lia` | Xavier Leroy | 2020-12-29 | 14 | -1026/+1022 |
| * | Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le | Xavier Leroy | 2020-12-29 | 2 | -13/+13 |
* | | Val_cmp* -> Val.mxcmp* | Sylvain Boulmé | 2021-01-07 | 2 | -0/+50 |
* | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 7 | -10/+279 |
|\ \ | |||||
| * \ | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 17 | -10/+1710 |
| |\ \ | |||||
| * \ \ | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 7 | -10/+279 |
| |\ \ \ | | | |/ | | |/| | |||||
| | * | | Support the use of already-installed MenhirLib and Flocq libraries | Xavier Leroy | 2020-09-21 | 2 | -4/+3 |
| | * | | Simplify two scripts in Zbits (#369) | Maxime Dénès | 2020-09-18 | 1 | -2/+2 |
| | * | | Use Hashtbl.find_opt. | Bernhard Schommer | 2020-06-28 | 1 | -1/+1 |
| | * | | Add a canonical encoding of identifiers as numbers and use it in clightgen (#... | Xavier Leroy | 2020-05-19 | 1 | -3/+76 |
| | * | | Move Commandline to the lib/ directory | Xavier Leroy | 2020-05-05 | 2 | -0/+196 |
| | * | | Import ListNotations explicitly | Xavier Leroy | 2020-05-04 | 1 | -0/+1 |
| | * | | Revert "Do not use the list notation `[]`" | Xavier Leroy | 2020-05-04 | 1 | -8/+8 |
| | * | | Do not use the list notation `[]` | Xavier Leroy | 2020-05-04 | 1 | -8/+8 |
* | | | | Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy... | David Monniaux | 2020-11-27 | 18 | -0/+1802 |
|\ \ \ \ | | |_|/ | |/| | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-19 | 1 | -10/+53 |
| |\ \ \ | |/ / / |/| | | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 1 | -0/+6 |
| |\| | | |||||
| * | | | fix issue 210 in simu_check | Sylvain Boulmé | 2020-09-21 | 1 | -4/+10 |
| * | | | starting to move common files | David Monniaux | 2020-09-16 | 16 | -0/+1651 |
* | | | | Proof of UnionFind.pathlen_union | Sylvain Boulmé | 2020-11-16 | 1 | -10/+53 |
| |/ / |/| | | |||||
* | | | centralize if_same | David Monniaux | 2020-10-09 | 1 | -0/+6 |
|/ / | |||||
* | | 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 |
| |\| | |