aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* moved stuff to appropriate places and removed irrelevant contentDavid Monniaux2022-02-111-0/+18
* Merge ../kvx-work into kvx_fp_divisionDavid Monniaux2022-02-031-2/+2
|\
| * 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
* | | moved functions to a more logical placeDavid Monniaux2022-01-131-165/+179
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_divisionDavid Monniaux2021-12-142-742/+915
|\| |
| * | 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
* | | Values: conversions to nearest intDavid Monniaux2021-12-121-0/+9
* | | _ne conversionsDavid Monniaux2021-12-121-0/+9
* | | progress on lemmasDavid Monniaux2021-12-121-1/+81
* | | minor implicit issueDavid Monniaux2021-12-101-2/+2
* | | more properties on ZnearestDavid Monniaux2021-12-101-2/+35
* | | factor proofsDavid Monniaux2021-12-101-1/+20
* | | factorize proofDavid Monniaux2021-12-101-28/+22
* | | beautify proofDavid Monniaux2021-12-101-24/+16
* | | ZofB_ne_correctDavid Monniaux2021-12-101-0/+10
* | | ZofB_ne_correctDavid Monniaux2021-12-101-2/+31
* | | progress on ZnearestEDavid Monniaux2021-12-101-24/+54
* | | ZofB_ne_correct unfinishedDavid Monniaux2021-12-081-1/+18
* | | Merge branch 'kvx_fp_division' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/...David Monniaux2021-12-071-1/+1
|\ \ \
| * | | ZnearestE_oppDavid Monniaux2021-12-071-4/+83
* | | | ZnearestE_oppDavid Monniaux2021-12-071-3/+121
|/ / /
* | | progress on ZofB_neDavid Monniaux2021-12-061-0/+51
* | | Zdiv_neDavid Monniaux2021-12-061-0/+11
|/ /
* | 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
generated by cgit (git 2.34.1) at 2024-04-27 08:43:32 +0000