Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | | 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 comev3.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 comev3.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 | |
* | | | Datatypes no longer shadows fst and snd | Bernhard Schommer | 2017-02-06 | 1 | -1/+1 | |
* | | | Remove open Locations. | Bernhard Schommer | 2017-02-06 | 1 | -6/+5 | |
* | | | Remove open Locations. | Bernhard Schommer | 2017-02-06 | 1 | -6/+5 | |
* | | | Remove open AST. | Bernhard Schommer | 2017-02-06 | 1 | -4/+3 |