aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-02-021-2/+2
|\
| * Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-101-2/+2
* | Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-012-742/+915
|\|
| * Maps.v: transparency of NodeXavier Leroy2021-11-161-1/+3
| * An improved PTree data structure (#420)Xavier Leroy2021-11-162-638/+902
* | option monad tacticSylvain Boulmé2021-11-061-1/+7
* | Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-292-23/+23
|\|
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-032-23/+23
* | 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
generated by cgit (git 2.34.1) at 2024-06-02 09:33:02 +0000