aboutsummaryrefslogtreecommitdiffstats
path: root/doc
Commit message (Collapse)AuthorAgeFilesLines
* link on Cyril's short videoSylvain Boulmé2020-10-191-2/+2
|
* update the title of our paperSylvain Boulmé2020-10-071-2/+2
|
* links to the impure library on githubSylvain Boulmé2020-07-311-1/+1
|
* Improving Coqdoc on abstractbbSylvain Boulmé2020-07-311-1/+1
|
* Improving the coqdocSylvain Boulmé2020-07-291-5/+5
|
* automatic date in the html indexSylvain Boulmé2020-05-281-1/+1
|
* source url in the docSylvain Boulmé2020-05-271-2/+4
|
* link to the HAL preprintSylvain Boulmé2020-05-271-2/+6
|
* k1c -> kvx changesDavid Monniaux2020-05-261-37/+37
|
* fix index-mppa_k1c.htmlSylvain Boulmé2020-05-111-1/+1
|
* updating the html index for mppa-k1cSylvain Boulmé2020-05-101-45/+27
| | | | NOTE: This file has been copied from the one of pldi-artefact branch.
* Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-011-1/+3
|\
| * Updates for release 3.7Xavier Leroy2020-03-311-1/+3
| |
* | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-201-2/+3
|\| | | | | | | mppa-work-upstream-merge
| * Update for release 3.6v3.6Xavier Leroy2019-09-171-2/+3
| |
* | Merge branch 'mppa-work' of ↵David Monniaux2019-09-101-0/+380
|\ \ | |/ |/| | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * a dedicated entry-point to the doc of Coq sourcesSylvain Boulmé2019-09-031-0/+380
| |
* | Update man page.Bernhard Schommer2019-09-021-1/+1
|/ | | | Unused-variables is disabled by default.
* More precise description of '-O0' and 'non-linear-cond-expr'Michael Schmidt2019-07-101-1/+2
|
* Update synonymous list for -O0, add new named warning classMichael Schmidt2019-07-051-1/+6
|
* Update documentation of -ObranchlessXavier Leroy2019-07-051-6/+8
| | | | Updated man page + better usage message.
* Updated man page.Bernhard Schommer2019-06-171-0/+10
|
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-1/+1
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+6
| | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
* Check for alignment of command-line switches.Bernhard Schommer2019-05-101-3/+3
| | | | | | Add a check for alignment on command-line switches `-falign-*`. The check is similar to the one for the alignment attribute and ensures that only powers of two can be specified.
* Update HTML doc for release 3.5Xavier Leroy2019-02-271-1/+1
|
* Fix some URLs in the first page of the Coq HTML documentation (#263)Andre2019-01-221-5/+5
| | | | Links to machine-specific modules were garbled during editing.
* Updates for release 3.4v3.4Xavier Leroy2018-09-171-1/+1
|
* document new named warning class 'reduced-alignment', bug 23389Michael Schmidt2018-09-041-0/+4
|
* Document new named warning for tentative static definitions with incomplete ↵Michael Schmidt2018-08-211-0/+4
| | | | type, bug 23377
* Document new named warning for flexible arrays, bug 23324Michael Schmidt2018-08-211-1/+1
|
* Document new named warning for flexible arrays, bug 23324Michael Schmidt2018-08-211-0/+4
|
* Remove undocumented option.Bernhard Schommer2018-08-071-4/+0
| | | | | The option -doptions was never document and no longer works. Bug 19775
* Typo in Ctyping entryXavier Leroy2018-06-171-1/+1
|
* bug 23325, document recently introduced named warningsMichael Schmidt2018-06-051-2/+2
|
* bug 23325, document recently introduced named warningsMichael Schmidt2018-06-051-3/+3
|
* bug 23325, document recently introduced named warningsMichael Schmidt2018-06-051-1/+1
|
* bug 23325, document recently introduced named warningsMichael Schmidt2018-06-051-4/+28
|
* bug 23325, document changed default for c11 named warningMichael Schmidt2018-06-051-1/+1
|
* Use the standalone coq2html tool to generate the HTML documentationXavier Leroy2018-06-015-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.3Xavier Leroy2018-05-301-1/+1
|
* coq2html: use OCaml's alternate string literals for multi-line stringsXavier Leroy2018-05-301-15/+15
|
* Update manpage for new warning name classMichael Schmidt2018-03-081-0/+4
|
* Preparations for release 3.2Xavier Leroy2018-01-131-4/+4
|
* Mention the RISC-V port as wellXavier Leroy2018-01-131-1/+1
|
* Update man page for new Diab target optionMichael Schmidt2018-01-081-6/+8
|
* Update man page for new Diab target optionMichael Schmidt2018-01-081-0/+6
|
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-071-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.1Xavier Leroy2017-08-181-23/+17
|
* Update documentation entry point for release 3.0 (retroactively)Xavier Leroy2017-07-131-5/+8
| | | | Some modules new in 3.0 were not mentioned.
generated by cgit (git 2.34.1) at 2024-07-02 11:56:24 +0000