Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | option monad tactic | Sylvain Boulmé | 2021-11-06 | 1 | -1/+7 |
* | Merge remote-tracking branch 'origin/master' into towards_3.10 | David Monniaux | 2021-10-29 | 2 | -23/+23 |
|\ | |||||
| * | Qualify `Instance` and `Program Instance` as `Global` | Xavier Leroy | 2021-10-03 | 2 | -23/+23 |
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10 | David Monniaux | 2021-09-24 | 5 | -4/+198 |
|\| | |||||
| * | Avoid `Global Set Asymmetric Patterns` (#408) | Xavier Leroy | 2021-09-15 | 4 | -2/+4 |
| * | Native support for bit fields (#400) | Xavier Leroy | 2021-08-22 | 1 | -0/+112 |
| * | Int.sign_ext_shr_shl: weaker hypothesis | Xavier Leroy | 2021-08-22 | 1 | -2/+2 |
| * | Add `floor` and some properties | Xavier Leroy | 2021-07-26 | 1 | -0/+37 |
| * | More lemmas about `align` | Xavier Leroy | 2021-07-26 | 1 | -0/+17 |
| * | More lemmas about list append | Xavier Leroy | 2021-07-26 | 1 | -0/+26 |
| * | Use the LGPL instead of the GPL for dual-licensed files | Xavier Leroy | 2021-05-08 | 31 | -124/+155 |
| * | Use List.repeat from Coq's standard library instead of list_repeat | Xavier Leroy | 2021-04-19 | 1 | -20/+0 |
* | | Merge branch 'kvx-work' into BTL | Léo Gourdin | 2021-06-10 | 33 | -1327/+1365 |
|\ \ | |||||
| * | | 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 |
* | | | better autodestruct ? | Sylvain Boulmé | 2021-05-11 | 1 | -1/+16 |
* | | | start the new "BTL" IR. | Sylvain Boulmé | 2021-04-28 | 1 | -0/+6 |
|/ / | |||||
* | | 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 |