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