aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
...
* | Add a man-pageMichael Schmidt2016-10-141-0/+2
|/
* fix merge conflictsMichael Schmidt2016-08-171-1/+2
|\
| * Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-201-1/+2
* | Implement support for big endian arm targets.Bernhard Schommer2016-08-051-0/+1
|/
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-8/+5
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-281-1/+0
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-2/+3
* Also enable warnings for doc generator.Bernhard Schommer2016-04-061-2/+2
* Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-1/+2
* Split up tools and options.Bernhard Schommer2016-02-251-1/+4
* Added configuration to enable clightgen build.Bernhard Schommer2015-12-281-10/+6
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-0/+1
* Removed the version from the compcert.ini file and add it again in a separate...Bernhard Schommer2015-07-011-11/+15
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-5/+4
* Merge branch 'master' into dwarfBernhard Schommer2015-03-311-0/+2
|\
| * Improvements in the StructReturn transformation (ABI conformance for passing ...Xavier Leroy2015-03-201-0/+2
* | Started implementing the printing functions for the debug info. Added a globa...Bernhard Schommer2015-03-161-0/+1
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-101-3/+3
|\|
| * Removed the glob files from doc/ instead of doc/glob/Bernhard Schommer2015-02-261-1/+1
| * Merge github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-191-1/+1
| |\
| * | Removed the linker flag again.Bernhard Schommer2015-01-201-2/+2
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-231-1/+1
|\ \ \ | | |/ | |/|
| * | Merge branch 'named-structs'Xavier Leroy2015-01-231-1/+1
| |\ \ | | |/ | |/|
| | * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-1/+1
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-201-4/+4
|\| |
| * | Renamed LIB into VLIB to avoid clashes with environment variables.Bernhard Schommer2015-01-201-2/+2
| * | Added variable to the Makefile to specify additional linker commands and chan...Bernhard Schommer2015-01-151-2/+2
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-121-48/+25
|\| |
| * | No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-181-0/+1
| * | Merge branch 'master' into pure-makefilesXavier Leroy2014-12-171-10/+12
| |\ \
| * | | Use OCaml's .opt compilers when available.Xavier Leroy2014-12-171-7/+9
| * | | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and p...Xavier Leroy2014-11-221-57/+23
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-171-15/+8
|\ \ \ \ | | |/ / | |/| |
| * | | Use cp instead of symbolic links for executables.Xavier Leroy2014-12-171-15/+8
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-111-10/+10
|\| | |
| * | | Preserve single quotes (e.g. in CPREPRO) when generating compcert.iniXavier Leroy2014-12-111-10/+10
| | |/ | |/|
* | | Merge branch 'master' into dwarfBernhard Schommer2014-11-271-0/+1
|\| |
| * | Verification of the Unusedglob pass (removal of unreferenced static global de...Xavier Leroy2014-11-241-0/+1
| |/
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-271-1/+0
|\|
| * Tune behavior wrt warnings:Xavier Leroy2014-10-241-1/+0
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-201-0/+1
|\|
| * Deactivated the warning for deprecated features for compilation of cchecklink...Bernhard Schommer2014-10-201-0/+1
* | Added a file containing definitions for the types used to store the debug inf...Bernhard Schommer2014-10-131-1/+1
|/
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-091-1/+1
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-071-2/+2
* Change the way the tools like the linker, assembler, etc. are specified by in...Bernhard Schommer2014-09-301-21/+23
* configure: distinguish between ABI and processor model.xleroy2014-07-291-1/+2
* Simplify COQINCLUDESxleroy2014-07-231-3/+2
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-231-4/+2
* Redundant -I in CAMLINCLUDESxleroy2014-07-231-2/+3
generated by cgit (git 2.34.1) at 2024-05-18 04:13:16 +0000