index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
lib
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge remote-tracking branch 'absint/master' into merge_absint
David Monniaux
2022-02-02
1
-2
/
+2
|
\
|
*
Adapt w.r.t. coq/coq#15442 (#425)
Pierre-Marie Pédrot
2022-01-10
1
-2
/
+2
*
|
Merge remote-tracking branch 'absint/master' into towards_3.10
David Monniaux
2021-12-01
2
-742
/
+915
|
\
|
|
*
Maps.v: transparency of Node
Xavier Leroy
2021-11-16
1
-1
/
+3
|
*
An improved PTree data structure (#420)
Xavier Leroy
2021-11-16
2
-638
/
+902
*
|
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
[next]