aboutsummaryrefslogtreecommitdiffstats
path: root/doc
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-4/+6
|\
| * Updates for release 3.8v3.8Xavier Leroy2020-11-161-4/+6
* | 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
* | 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 mppa-work-upstrea...David Monniaux2019-09-201-2/+3
|\|
| * Update for release 3.6v3.6Xavier Leroy2019-09-171-2/+3
* | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-09-101-0/+380
|\ \ | |/ |/|
| * 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
|/
* 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.Bernhard Schommer2019-06-171-0/+10
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-1/+1
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+6
* Check for alignment of command-line switches.Bernhard Schommer2019-05-101-3/+3
* 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
* 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 t...Michael Schmidt2018-08-211-0/+4
* 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
* 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
* 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