aboutsummaryrefslogtreecommitdiffstats
path: root/doc
Commit message (Collapse)AuthorAgeFilesLines
* Allocproof linkLéo Gourdin2021-12-081-1/+1
|
* LICENSELéo Gourdin2021-12-081-1/+1
|
* docLéo Gourdin2021-12-071-37/+226
|
* improvement in html doc (not finished yet)Léo Gourdin2021-12-061-22/+145
|
* [Cherry picking] 01ade46b340267d8782c413f6bd5a3cff13ef0a6Léo Gourdin2021-12-061-0/+395
| | | | starting a new index-verimag.html on BTL doc
* Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-012-7/+2
|\ | | | | | | Mostly changes in PTree
| * mention AArch64 in man-pageMichael Schmidt2021-11-171-1/+1
| |
| * Remove documentation of bitfield language support option.Michael Schmidt2021-11-171-5/+0
| |
| * First update for release 3.10Xavier Leroy2021-11-161-1/+1
| |
| * Update for release 3.9Xavier Leroy2021-05-091-4/+5
| | | | | | | | Also: limit the max width of the page, to avoid very long lines.
* | Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-172-6/+6
| | | | | | | | To respect the symmetry between RTL- and LTL-Tunneling
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-1/+1
|\ \
| * | fix broken link in index-kvx.htmlSylvain Boulmé2021-04-161-1/+1
| | |
* | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-4/+5
|/ / | | | | | | cfrontend/C2C.ml
* | update index-kvx.htmlSylvain Boulmé2021-01-071-8/+8
| |
* | add profiling entry-points in the htmldoc.Sylvain Boulmé2020-12-171-2/+20
| |
* | add superblock-scheduling passes in the coqhtmlSylvain Boulmé2020-12-161-25/+62
| |
* | update the doc for CompCert 3.8Sylvain Boulmé2020-12-161-6/+12
| |
* | 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
| | | | | | | | 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
generated by cgit (git 2.34.1) at 2024-05-09 02:29:06 +0000