aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-245-4/+198
|\
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-154-2/+4
| * Native support for bit fields (#400)Xavier Leroy2021-08-221-0/+112
| * Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
| * Add `floor` and some propertiesXavier Leroy2021-07-261-0/+37
| * More lemmas about `align`Xavier Leroy2021-07-261-0/+17
| * More lemmas about list appendXavier Leroy2021-07-261-0/+26
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0831-124/+155
| * Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-191-20/+0
* | Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-1033-1327/+1365
|\ \
| * | coq 8.13.2David Monniaux2021-06-071-2/+1
| * | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-0131-144/+155
| * | replacing omega with lia in some fileLéo Gourdin2021-03-292-32/+34
| * | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2315-1150/+1176
| |\|
| | * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-213-33/+36
| | * Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
| | * Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| | * Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
| | * Replace `omega` tactic with `lia`Xavier Leroy2020-12-2914-1026/+1022
| | * Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
* | | better autodestruct ?Sylvain Boulmé2021-05-111-1/+16
* | | start the new "BTL" IR.Sylvain Boulmé2021-04-281-0/+6
|/ /
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-072-0/+50
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-177-10/+279
|\ \
| * \ Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0417-10/+1710
| |\ \
| * \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-187-10/+279
| |\ \ \ | | | |/ | | |/|
| | * | Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-212-4/+3
| | * | Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
| | * | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | * | Add a canonical encoding of identifiers as numbers and use it in clightgen (#...Xavier Leroy2020-05-191-3/+76
| | * | Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+196
| | * | Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| | * | Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| | * | Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
* | | | Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...David Monniaux2020-11-2718-0/+1802
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-191-10/+53
| |\ \ \ | |/ / / |/| | |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+6
| |\| |
| * | | fix issue 210 in simu_checkSylvain Boulmé2020-09-211-4/+10
| * | | starting to move common filesDavid Monniaux2020-09-1616-0/+1651
* | | | Proof of UnionFind.pathlen_unionSylvain Boulmé2020-11-161-10/+53
| |/ / |/| |
* | | centralize if_sameDavid Monniaux2020-10-091-0/+6
|/ /
* | Adding copyrightsCyril SIX2020-05-044-0/+48
* | moved to extraDavid Monniaux2020-04-161-0/+0
* | gmap2_idemDavid Monniaux2020-04-161-65/+111
* | gmap2_idemDavid Monniaux2020-04-161-0/+16
* | gmap2_idem_EmptyDavid Monniaux2020-04-161-0/+54
* | begin HashedMapsDavid Monniaux2020-04-161-0/+332
* | forward_move_lDavid Monniaux2020-03-101-1/+13
* | kill_reg_soundDavid Monniaux2020-03-091-1/+1
* | CSE3 generate lists of killableDavid Monniaux2020-03-051-0/+4
generated by cgit (git 2.34.1) at 2024-06-02 15:51:53 +0000