aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Release 3.0.1 here we comev3.0.1Xavier Leroy2017-02-142-1/+7
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-134-13/+21
* Turn warning "deprecated-implicit-arguments" off while compiling FlocqXavier Leroy2017-02-131-1/+4
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-138-19/+17
* Use "Local" as prefixXavier Leroy2017-02-1322-38/+36
* ARM, PowerPC: update Asmgenproof for Coq 8.6Xavier Leroy2017-02-132-14/+21
* Update Flocq to version 2.5.2Xavier Leroy2017-02-138-132/+91
* Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maxime...Xavier Leroy2017-02-139-19/+22
|\
| * Bump required version of Menhir to 20161201.Maxime Dénès2017-01-091-1/+1
| * Some backward compatible Ltac fixes, necessary for 8.6.Maxime Dénès2017-01-091-5/+7
| * Fix broken fragile automation.Maxime Dénès2017-01-091-1/+2
| * Configure now expects to find Coq 8.6.0.Maxime Dénès2017-01-091-3/+3
| * Subst's behavior on let-ins has changed.Maxime Dénès2017-01-091-2/+2
| * An hypothesis has changed name.Maxime Dénès2017-01-091-1/+1
| * The contradiction tactic has become more powerful.Maxime Dénès2017-01-091-2/+1
| * Intro patterns have changed semantics...Maxime Dénès2017-01-091-0/+1
| * The subst tactic has become more powerful.Maxime Dénès2017-01-093-4/+4
* | Release 3.0 here we comev3.0Xavier Leroy2017-02-102-2/+3
* | OS X: emit jumptables in .text segment, not .const segmentXavier Leroy2017-02-101-1/+1
* | Use Printf.sprintf instead of Format.sprintf when possibleXavier Leroy2017-02-091-4/+4
* | More tweaking of module 'open'Xavier Leroy2017-02-091-8/+10
* | Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-02-081-0/+7
|\ \
| * | Changelog update concerning attribute handlingXavier Leroy2017-02-071-0/+7
* | | Revert broken change to Cutil.Bernhard Schommer2017-02-083-10/+10
|/ /
* | Merge branch 'master' of ssh://github.com/AbsInt/CompCertXavier Leroy2017-02-063-83/+36
|\ \
| * | Simplified DebugInformation interface.Bernhard Schommer2017-02-063-83/+36
* | | Merge branch 'elaboration-of-attributes'Xavier Leroy2017-02-0611-47/+148
|\ \ \ | |/ / |/| |
| * | Preliminary support for the "noreturn" attributeXavier Leroy2017-02-062-12/+17
| * | Refactor the classification of attributesXavier Leroy2017-02-037-23/+101
| * | Use C99 syntax to print attributes over array typesXavier Leroy2017-02-011-4/+5
| * | Regression: type attributes and array modifiersXavier Leroy2017-02-011-2/+4
| * | Revised elaboration of attributesXavier Leroy2017-01-318-22/+38
* | | Cleanup opensBernhard Schommer2017-02-061-69/+62
* | | Removed shadowing open.Bernhard Schommer2017-02-061-11/+11
* | | Removed shadowing openBernhard Schommer2017-02-061-5/+5
* | | Remove shadowing openBernhard Schommer2017-02-061-1/+1
* | | Remove unused open.Bernhard Schommer2017-02-061-1/+0
* | | Cleanup opens.Bernhard Schommer2017-02-061-9/+8
* | | Generalized function to allow adding hex strings.Bernhard Schommer2017-02-062-4/+8
* | | Removed shadowing problems.Bernhard Schommer2017-02-061-9/+9
* | | Inlined open of ASTBernhard Schommer2017-02-061-7/+6
* | | Inlined open of ErrorsBernhard Schommer2017-02-061-10/+9
* | | Datatypes no longer shadows fst and sndBernhard Schommer2017-02-061-1/+1
* | | Remove open Locations.Bernhard Schommer2017-02-061-6/+5
* | | Remove open Locations.Bernhard Schommer2017-02-061-6/+5
* | | Remove open AST.Bernhard Schommer2017-02-061-4/+3
* | | Remove unused openBernhard Schommer2017-02-061-1/+0
* | | Remove unused openBernhard Schommer2017-02-061-1/+0
* | | Inline fst and snd from Datatypes.Bernhard Schommer2017-02-061-0/+4
* | | Removed the open AST.Bernhard Schommer2017-02-062-10/+8
generated by cgit (git 2.34.1) at 2024-05-19 23:26:56 +0000