| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Use the standalone coq2html tool to generate the HTML documentation | Xavier Leroy | 2018-06-01 | 5 | -752/+115 |
| | | | | | | coq2html is now a standalone project (https://github.com/xavierleroy/coq2html) packaged as coq-coq2html in OPAM-Coq. | ||||
| * | Update for release 3.3v3.3 | Xavier Leroy | 2018-05-30 | 1 | -1/+1 |
| | | |||||
| * | coq2html: use OCaml's alternate string literals for multi-line strings | Xavier Leroy | 2018-05-30 | 1 | -15/+15 |
| | | |||||
| * | Update manpage for new warning name class | Michael Schmidt | 2018-03-08 | 1 | -0/+4 |
| | | |||||
| * | Preparations for release 3.2 | Xavier Leroy | 2018-01-13 | 1 | -4/+4 |
| | | |||||
| * | Mention the RISC-V port as well | Xavier Leroy | 2018-01-13 | 1 | -1/+1 |
| | | |||||
| * | Update man page for new Diab target option | Michael Schmidt | 2018-01-08 | 1 | -6/+8 |
| | | |||||
| * | Update man page for new Diab target option | Michael Schmidt | 2018-01-08 | 1 | -0/+6 |
| | | |||||
| * | Inlining of static functions which are only called once. (#37) | Bernhard Schommer | 2017-12-07 | 1 | -0/+5 |
| | | | | | | | | | | New inlining heuristic for static functions. Static functions that are only called once can always be inlined, since they can be removed safely after inlining and no call prologue, epilogue, as well as register saving and needs to be generated. | ||||
| * | Update documentation index for release 3.1v3.1 | Xavier Leroy | 2017-08-18 | 1 | -23/+17 |
| | | |||||
| * | Update documentation entry point for release 3.0 (retroactively) | Xavier Leroy | 2017-07-13 | 1 | -5/+8 |
| | | | | | Some modules new in 3.0 were not mentioned. | ||||
| * | Add optimization option finline. | Bernhard Schommer | 2017-04-07 | 1 | -0/+5 |
| | | | | | | | The new option f(no-)inline controlls whether inlining is active or not. Bug 21343. | ||||
| * | update manpage for new options | Michael Schmidt | 2017-02-21 | 1 | -4/+16 |
| | | |||||
| * | drop .cm support from man page | Michael Schmidt | 2017-02-15 | 1 | -4/+0 |
| | | |||||
| * | mention share directory for -target option | Michael Schmidt | 2017-01-26 | 1 | -0/+1 |
| | | |||||
| * | describe -conf and -target | Michael Schmidt | 2017-01-26 | 1 | -0/+11 |
| | | |||||
| * | describe environment variable for configuration file | Michael Schmidt | 2017-01-26 | 1 | -2/+10 |
| | | |||||
| * | bug 20679, more precise description of -g | Michael Schmidt | 2017-01-17 | 1 | -1/+1 |
| | | |||||
| * | Fix typos | Michael Schmidt | 2017-01-04 | 1 | -2/+2 |
| | | |||||
| * | bug 20593, document new warning class in man-page | Michael Schmidt | 2016-12-14 | 1 | -0/+4 |
| | | |||||
| * | fix targets in section for code generation options | Michael Schmidt | 2016-12-02 | 1 | -1/+5 |
| | | |||||
| * | update info about x86 in manpage | Michael Schmidt | 2016-11-03 | 1 | -2/+2 |
| | | |||||
| * | Minor improvements | Michael Schmidt | 2016-10-17 | 1 | -4/+4 |
| | | |||||
| * | Update description for debugging options | Michael Schmidt | 2016-10-14 | 1 | -4/+3 |
| | | |||||
| * | Add a man-page | Michael Schmidt | 2016-10-14 | 1 | -0/+534 |
| | | |||||
| * | Update in preparation for release 2.7 | Xavier Leroy | 2016-06-22 | 1 | -3/+3 |
| | | |||||
| * | Also enable warnings for doc generator. | Bernhard Schommer | 2016-04-06 | 1 | -6/+6 |
| | | |||||
| * | Upgrade for release 2.6. | Xavier Leroy | 2015-12-21 | 1 | -1/+8 |
| | | |||||
| * | Updated PR by removing whitespaces. Bug 17450. | Bernhard Schommer | 2015-10-20 | 1 | -5/+5 |
| | | |||||
| * | Preserve ordinary comments within proof scripts. | Xavier Leroy | 2015-06-11 | 2 | -6/+31 |
| | | |||||
| * | Update for release 2.5. | Xavier Leroy | 2015-06-11 | 1 | -6/+15 |
| | | |||||
| * | Update Coq documentationv2.3 | xleroy | 2014-05-05 | 1 | -3/+3 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2483 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Updates for release 2.2 | xleroy | 2014-02-21 | 2 | -5/+28 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2415 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Late update for release 2.1. | xleroy | 2013-10-28 | 1 | -1/+1 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2359 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Version 2.00 -> version 2.0v2.0 | xleroy | 2013-06-21 | 1 | -1/+1 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Updates in preparation for release 2.00 | xleroy | 2013-06-19 | 1 | -47/+16 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Use "-as" to put CompCert modules in a compcert.xxx namespace. | xleroy | 2013-05-01 | 1 | -6/+14 |
| | | | | | | | | | Simplified the scripts "coq" and "pg". Updated deps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Updating doc for 1.13 | xleroy | 2013-03-11 | 1 | -8/+5 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2142 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Updated documentationv1.12 | xleroy | 2013-01-11 | 2 | -14/+14 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2098 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Update for release 1.12 | xleroy | 2013-01-09 | 1 | -3/+8 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2097 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Make Clight independent of CompCert C. | xleroy | 2012-10-08 | 1 | -1/+4 |
| | | | | | | | | Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Late update for 1.11 | xleroy | 2012-07-13 | 1 | -4/+6 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1977 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Merge of the newmem branch: | xleroy | 2012-05-21 | 1 | -1/+18 |
| | | | | | | | | | | | - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | MAJ docv1.10 | xleroy | 2012-03-12 | 1 | -11/+5 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1850 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Doc fixes | xleroy | 2011-08-23 | 2 | -2/+3 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1726 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Changelog, doc: updated for release 1.9v1.9 | xleroy | 2011-08-22 | 1 | -1/+9 |
| | | | | | | | | lib/Integers, Makefile: unsuccessful experiments with coqchk git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1723 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Update for release 1.8.2 | xleroy | 2011-05-24 | 1 | -29/+38 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1656 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Renamed Machconcr into Machsem. | xleroy | 2011-04-09 | 1 | -2/+1 |
| | | | | | | | | | Removed Machabstr and Machabstr2concr, now useless following the reengineering of Stacking. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1633 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Update for 1.8.1 | xleroy | 2011-03-14 | 1 | -2/+2 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1609 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Update for release 1.8 | xleroy | 2010-09-21 | 1 | -5/+12 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
 |
index : compcert | |
| CompCert fork with minor modifications for Vericert. |
| aboutsummaryrefslogtreecommitdiffstats |