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
...
|
*
|
Revised, more precise implementation of control-flow analysis
Xavier Leroy
2017-02-07
1
-48
/
+98
|
*
|
Control-flow analysis: wrong flow for "case"/"default" statements
Xavier Leroy
2017-02-07
1
-4
/
+6
|
*
|
More precise warnings about function returns
Xavier Leroy
2017-02-07
5
-32
/
+237
*
|
|
Remove tests involving Cminor concrete syntax. Update Changelog
Xavier Leroy
2017-02-15
29
-3336
/
+3
*
|
|
Merge pull request #170 from AbsInt/remove_cminor
Xavier Leroy
2017-02-15
9
-1379
/
+3
|
\
\
\
|
*
|
|
Removed CMinor import. Bug 20992
Bernhard Schommer
2017-02-14
9
-1379
/
+3
*
|
|
|
Removed superfluous semicolon.
Bernhard Schommer
2017-02-14
1
-1
/
+1
|
/
/
/
*
|
|
Remove Optionsprinter. Bug 20993
Bernhard Schommer
2017-02-14
2
-155
/
+1
*
|
|
Release 3.0.1 here we come
v3.0.1
Xavier Leroy
2017-02-14
2
-1
/
+7
*
|
|
Give explicit scopes to notations a#b and a##b and a#b<-c
Xavier Leroy
2017-02-13
4
-13
/
+21
*
|
|
Turn warning "deprecated-implicit-arguments" off while compiling Flocq
Xavier Leroy
2017-02-13
1
-1
/
+4
*
|
|
Replace "Implicit Arguments" with "Arguments"
Xavier Leroy
2017-02-13
8
-19
/
+17
*
|
|
Use "Local" as prefix
Xavier Leroy
2017-02-13
22
-38
/
+36
*
|
|
ARM, PowerPC: update Asmgenproof for Coq 8.6
Xavier Leroy
2017-02-13
2
-14
/
+21
*
|
|
Update Flocq to version 2.5.2
Xavier Leroy
2017-02-13
8
-132
/
+91
*
|
|
Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maxime...
Xavier Leroy
2017-02-13
9
-19
/
+22
|
\
\
\
|
|
_
|
/
|
/
|
|
|
*
|
Bump required version of Menhir to 20161201.
Maxime Dénès
2017-01-09
1
-1
/
+1
|
*
|
Some backward compatible Ltac fixes, necessary for 8.6.
Maxime Dénès
2017-01-09
1
-5
/
+7
|
*
|
Fix broken fragile automation.
Maxime Dénès
2017-01-09
1
-1
/
+2
|
*
|
Configure now expects to find Coq 8.6.0.
Maxime Dénès
2017-01-09
1
-3
/
+3
|
*
|
Subst's behavior on let-ins has changed.
Maxime Dénès
2017-01-09
1
-2
/
+2
|
*
|
An hypothesis has changed name.
Maxime Dénès
2017-01-09
1
-1
/
+1
|
*
|
The contradiction tactic has become more powerful.
Maxime Dénès
2017-01-09
1
-2
/
+1
|
*
|
Intro patterns have changed semantics...
Maxime Dénès
2017-01-09
1
-0
/
+1
|
*
|
The subst tactic has become more powerful.
Maxime Dénès
2017-01-09
3
-4
/
+4
*
|
|
Release 3.0 here we come
v3.0
Xavier Leroy
2017-02-10
2
-2
/
+3
*
|
|
OS X: emit jumptables in .text segment, not .const segment
Xavier Leroy
2017-02-10
1
-1
/
+1
*
|
|
Use Printf.sprintf instead of Format.sprintf when possible
Xavier Leroy
2017-02-09
1
-4
/
+4
*
|
|
More tweaking of module 'open'
Xavier Leroy
2017-02-09
1
-8
/
+10
*
|
|
Merge branch 'master' of github.com:AbsInt/CompCert
Bernhard Schommer
2017-02-08
1
-0
/
+7
|
\
\
\
|
*
|
|
Changelog update concerning attribute handling
Xavier Leroy
2017-02-07
1
-0
/
+7
|
|
|
/
|
|
/
|
*
/
|
Revert broken change to Cutil.
Bernhard Schommer
2017-02-08
3
-10
/
+10
|
/
/
*
|
Merge branch 'master' of ssh://github.com/AbsInt/CompCert
Xavier Leroy
2017-02-06
3
-83
/
+36
|
\
\
|
*
|
Simplified DebugInformation interface.
Bernhard Schommer
2017-02-06
3
-83
/
+36
*
|
|
Merge branch 'elaboration-of-attributes'
Xavier Leroy
2017-02-06
11
-47
/
+148
|
\
\
\
|
|
/
/
|
/
|
|
|
*
|
Preliminary support for the "noreturn" attribute
Xavier Leroy
2017-02-06
2
-12
/
+17
|
*
|
Refactor the classification of attributes
Xavier Leroy
2017-02-03
7
-23
/
+101
|
*
|
Use C99 syntax to print attributes over array types
Xavier Leroy
2017-02-01
1
-4
/
+5
|
*
|
Regression: type attributes and array modifiers
Xavier Leroy
2017-02-01
1
-2
/
+4
|
*
|
Revised elaboration of attributes
Xavier Leroy
2017-01-31
8
-22
/
+38
*
|
|
Cleanup opens
Bernhard Schommer
2017-02-06
1
-69
/
+62
*
|
|
Removed shadowing open.
Bernhard Schommer
2017-02-06
1
-11
/
+11
*
|
|
Removed shadowing open
Bernhard Schommer
2017-02-06
1
-5
/
+5
*
|
|
Remove shadowing open
Bernhard Schommer
2017-02-06
1
-1
/
+1
*
|
|
Remove unused open.
Bernhard Schommer
2017-02-06
1
-1
/
+0
*
|
|
Cleanup opens.
Bernhard Schommer
2017-02-06
1
-9
/
+8
*
|
|
Generalized function to allow adding hex strings.
Bernhard Schommer
2017-02-06
2
-4
/
+8
*
|
|
Removed shadowing problems.
Bernhard Schommer
2017-02-06
1
-9
/
+9
*
|
|
Inlined open of AST
Bernhard Schommer
2017-02-06
1
-7
/
+6
*
|
|
Inlined open of Errors
Bernhard Schommer
2017-02-06
1
-10
/
+9
[prev]
[next]