index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
More efficient test for powers of two
Xavier Leroy
2019-05-09
2
-26
/
+105
*
Make scripts compatible with new behavior of field_simplify (#291)
Vincent Laporte
2019-05-06
2
-3
/
+3
*
Rename Fappli_IEEE_extra.v into IEEE754_extra.v
Xavier Leroy
2019-04-26
3
-2
/
+2
*
Move Z definitions out of Integers and into Zbits
Xavier Leroy
2019-04-26
13
-884
/
+1031
*
lib/Coqlib.v: remove defns about multiplication, division, modulus
Xavier Leroy
2019-04-23
15
-135
/
+52
*
Replace nat_of_Z with Z.to_nat
Xavier Leroy
2019-04-23
11
-68
/
+45
*
Problems with Dwarf ranges (#159)
Xavier Leroy
2019-04-23
9
-56
/
+96
|
\
|
*
Simplified offset printing.
Bernhard Schommer
2019-04-16
1
-2
/
+3
|
*
Print only debug info for printed functions.
Bernhard Schommer
2019-04-16
6
-14
/
+18
|
*
Reworked range entries.
Bernhard Schommer
2019-04-16
3
-39
/
+71
|
*
Reset scope ids later.
Bernhard Schommer
2019-04-16
1
-1
/
+1
|
*
Avoid generation of empty ranges.
Bernhard Schommer
2019-04-16
1
-1
/
+4
|
*
Relax requirement for ranges for compilation unit.
Bernhard Schommer
2019-04-16
1
-1
/
+1
|
/
*
Typo in comment about Ijumptable in RTL.v
Alix Trieu
2019-04-15
1
-1
/
+1
*
Fix typo in section name in Selectionproof.v
Alix Trieu
2019-04-15
1
-2
/
+2
*
Floats.v: remove leftover Print commands
Xavier Leroy
2019-04-04
1
-5
/
+1
*
Floats.v: avoid using module Zlogarithm in the proofs
Xavier Leroy
2019-04-03
1
-10
/
+19
*
Correct typo in Clightnorm.ml (#285)
Alix Trieu
2019-03-27
1
-1
/
+1
*
Ignore more of Coq's cache files
Xavier Leroy
2019-03-27
1
-1
/
+4
*
Upgrade embedded version of Flocq to 3.1.
Guillaume Melquiond
2019-03-27
46
-7841
/
+9954
*
Define macros with CompCert's version number (#284)
Xavier Leroy
2019-03-27
1
-2
/
+24
*
Harden configure against weird Menhir installations
Xavier Leroy
2019-03-25
1
-2
/
+8
*
RTLgenproof: destruct too deep
Xavier Leroy
2019-03-25
1
-2
/
+2
*
Integers.v: add modulus_gt_one (#259)
Xavier Leroy
2019-03-25
1
-1
/
+7
*
Update the comment of the free operation (#277)
chaomaer
2019-03-25
1
-1
/
+1
*
Minor simplifications in two proofs. (#280)
Vincent Laporte
2019-03-25
2
-3
/
+3
*
Improve overflow check for integer literals (#157)
Michael Schmidt
2019-03-20
1
-2
/
+4
*
Update version number for 3.5
v3.5
Xavier Leroy
2019-02-28
1
-1
/
+1
*
Update HTML doc for release 3.5
Xavier Leroy
2019-02-27
1
-1
/
+1
*
Update Changelog in preparation for release 3.5
Xavier Leroy
2019-02-26
1
-1
/
+1
*
Maximum supported Menhir version (#275)
Xavier Leroy
2019-02-26
1
-1
/
+1
*
Update Changelog in preparation for release 3.5
Xavier Leroy
2019-02-25
1
-0
/
+35
*
Maximum supported Menhir version (#275)
Jacques-Henri Jourdan
2019-02-25
1
-2
/
+3
*
Revised attachment of name attributes to structs, unions, enums
Xavier Leroy
2019-02-25
3
-6
/
+29
*
Reject object-related and struct-related attributes on typedefs
Xavier Leroy
2019-02-25
4
-8
/
+19
*
Add regression test for "aligned" attribute
Xavier Leroy
2019-02-25
3
-1
/
+120
*
Distinguish object-related and name-related attributes
Xavier Leroy
2019-02-25
4
-13
/
+24
*
Do not expand type names when floating attributes "up" a declaration
Xavier Leroy
2019-02-25
3
-2
/
+24
*
Ignore and clean file .lia.cache
Xavier Leroy
2019-02-12
2
-1
/
+4
*
Make the checker happy (#272)
Vincent Laporte
2019-02-12
3
-19
/
+17
*
Add support for Coq 8.9.0
Xavier Leroy
2019-02-04
1
-3
/
+3
*
<stddef.h>: define NULL with type void *
Xavier Leroy
2019-02-04
1
-1
/
+1
*
Test for NULL in variable argument lists
Xavier Leroy
2019-02-04
2
-1
/
+53
*
<stdbool.h>: add missing macro __bool_true_false_are_defined
Xavier Leroy
2019-02-04
1
-0
/
+1
*
Fix some URLs in the first page of the Coq HTML documentation (#263)
Andre
2019-01-22
1
-5
/
+5
*
Use `Program Instance` instead of `Instance` + refine mode (#261)
Maxime Dénès
2018-12-27
2
-64
/
+86
*
x86: wrong modeling of ZF flag for FP comparisons
Xavier Leroy
2018-12-20
2
-130
/
+66
*
Add functions "ordered" and "compare" to Float and Float32
Xavier Leroy
2018-12-20
1
-9
/
+20
*
Fix fixme in PackedStructs.
Bernhard Schommer
2018-11-20
1
-4
/
+4
*
Fix typo in asmexpand. Bug 24953
Bernhard Schommer
2018-11-07
1
-1
/
+1
[prev]
[next]