aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* 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 cp instead of symbolic links for executables.Xavier Leroy2014-12-171-15/+8
| * Preserve single quotes (e.g. in CPREPRO) when generating compcert.iniXavier Leroy2014-12-111-10/+10
| * Verification of the Unusedglob pass (removal of unreferenced static global de...Xavier Leroy2014-11-241-0/+1
* | 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
|/
* Tune behavior wrt warnings:Xavier Leroy2014-10-241-1/+0
* Deactivated the warning for deprecated features for compilation of cchecklink...Bernhard Schommer2014-10-201-0/+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
* Merge of "newspilling" branch:xleroy2014-07-231-1/+2
* Update Coq documentationv2.3xleroy2014-05-051-1/+1
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-3/+18
* ia32/Select*: complete the modifications to shifts.xleroy2014-04-111-7/+8
* Merge of branch linear-typing:xleroy2014-04-061-1/+1
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-1/+1
* Move wt_instr_inv where it belongs.xleroy2014-03-271-1/+1
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-1/+1
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-1/+1
* Merge of branch value-analysis.xleroy2013-12-201-2/+4
* powerpc/: new unary operation "addsymbol"xleroy2013-11-171-1/+1
* Merge of Flocq version 2.2.0.xleroy2013-08-021-10/+12
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-2/+2
* Updating LICENSE and license headers, continued.xleroy2013-06-171-0/+3
* Fix compilation of runtime system.xleroy2013-05-291-0/+4
* Merge of the float32 branch: xleroy2013-05-191-1/+1
* Preliminary support for debugging info (-g).xleroy2013-05-171-0/+1
* Clean up 'make clean'xleroy2013-05-011-2/+1
* Use "-as" to put CompCert modules in a compcert.xxx namespace.xleroy2013-05-011-7/+16
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-11/+8
* Updated issues with coqchk. See PR#3026 on the Coq bug tracker.xleroy2013-04-141-6/+9
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-1/+1
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-4/+3
* More correct exportclight/ dependenciesxleroy2013-01-081-2/+2
* Put clighgen files in exportclight/xleroy2013-01-051-7/+10
* RTLgenaux: heuristic to orient if-then-else statements based on sizes.xleroy2012-12-311-2/+4
* Make "all" the defaut target.xleroy2012-12-291-18/+21
* Merge of the clightgen branch:xleroy2012-12-291-2/+11
* Clight: split off the big step semantics in ClightBigstep.xleroy2012-10-141-1/+1
* Make Clight independent of CompCert C.xleroy2012-10-081-1/+1
* Support for indirect symbols under MacOS X (final).xleroy2012-07-141-1/+1
* Revert unintentional commit #1955xleroy2012-07-061-6/+6
* Ajout trunk CompCertblazy2012-07-041-6/+6
* Use Flocq for floatsxleroy2012-06-281-2/+14
generated by cgit (git 2.34.1) at 2024-06-02 22:38:48 +0000