75 Commits

Author SHA1 Message Date
Claude Marche
e5f6a089fe fix doc of for loops 2025-11-19 13:18:39 +01:00
Li-yao Xia
9cd080a32f doc: exclude '_' from lident_nq 2025-05-13 10:48:09 +02:00
Guillaume Melquiond
6db1a4816f Merge branch 'bugfix/v1.8' 2025-05-02 15:51:23 +02:00
Li-yao Xia
0687abff5e doc: Fix production rules for suffix, lident_nq, uident_nq, qident to agree with lexer.mll 2025-04-09 15:46:38 +02:00
Guillaume Melquiond
3f66c6e298 Use more links to the standard library in the documentation. 2024-12-16 15:49:10 +01:00
Guillaume Melquiond
59fde1a829 Fix some documentation typos. 2024-12-16 15:49:10 +01:00
Jean-Christophe Filliâtre
93d4646a98 improved documentation 2024-11-27 15:38:02 +01:00
Loïc Correnson
e2afddb11d Resolve "Add injectivity for type invariant" 2024-01-31 13:02:13 +00:00
Guillaume Melquiond
2448efa66e Update URL to the website. 2024-01-19 22:17:03 +01:00
François Bobot
5019447d79 [Doc] interface 2023-05-23 14:05:34 +02:00
MARCHE Claude
39a6cac355 Parser accepts ident after variant
propagate attributes on a variant to the enclosing formula
2023-04-04 12:34:26 +00:00
Claude Marche
ba4a0fae8e doc 2023-02-06 10:37:02 +01:00
Benjamin Jorge
a957074a39 Forbid using different names for constructors, fields, and (co)inductive cases 2023-01-26 14:20:10 +01:00
Benjamin Jorge
8cf6e12afb Add some documentation 2023-01-23 11:00:36 +01:00
Guillaume Melquiond
dc0208ab63 Improve organization of documentation. 2022-05-11 14:40:02 +02:00
Jean-Christophe Filliatre
b6d24864da doc: mutually recursive types and functions 2022-04-25 14:44:33 +02:00
François Bobot
09e8a348c1 Merge remote-tracking branch 'origin/master' into generalize_witness 2021-04-24 21:22:38 +02:00
Guillaume Melquiond
84026c7995 Homogenize index entries for keywords. 2021-04-09 11:57:42 +02:00
Guillaume Melquiond
fd2a412add Merge documentation sections about "at" and "old". 2021-04-09 11:36:08 +02:00
Guillaume Melquiond
21d3019da4 Fix index entries. 2021-04-09 11:26:02 +02:00
Xavier Denis
f810d72828 Document the syntax of break and continue 2021-02-01 12:17:01 +01:00
Jean-Christophe Filliatre
0ad5c1eb70 doc: improved paragraph related to old and at 2021-01-28 09:20:53 +01:00
Claude Marche
0bafaf42fe better make some rubrics as sub-sections 2021-01-27 15:25:45 +01:00
Claude Marche
dbb182330d documentation for any 2021-01-27 15:18:42 +01:00
Guillaume Melquiond
673aa6cd45 Move the generation of library-*.dot files to Makefile.
Files are generated in the "build-latest" job and are propagated to the
"doc" job using artifacts, which eliminates the need for a dedicated
Makefile. This forces us to move the "doc" job to the "test" stage.
2021-01-23 16:20:48 +01:00