index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
/
language
/
core
/
inductive.rst
Age
Commit message (
Expand
)
Author
2021-03-08
Convert 2nd part of rewriting chapter to prodn
Jim Fehrle
2020-12-30
Convert rewriting and proof-mode chapters to prodn
Jim Fehrle
2020-11-26
[attributes] [typing] Rename `typing` to `bypass_check`
Emilio Jesus Gallego Arias
2020-11-26
[attributes] [doc] Documentation review by Théo.
Emilio Jesus Gallego Arias
2020-11-26
[vernac] Allow to control typing flags with attributes.
Emilio Jesus Gallego Arias
2020-11-24
Convert auto chapter to prodn
Jim Fehrle
2020-11-18
Review commit: improving the doc of boolean attributes.
Théo Zimmermann
2020-11-18
[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.
Emilio Jesus Gallego Arias
2020-11-16
Update grammar in doc
Jim Fehrle
2020-11-16
Doc for variance syntax
Gaëtan Gilbert
2020-11-09
[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.
Théo Zimmermann
2020-11-02
[doc] attribute #[using]
Enrico Tassi
2020-10-27
Change a few nonterminal names in mlgs and update doc to match
Jim Fehrle
2020-10-24
Convert misc chapters to prodn
Jim Fehrle
2020-10-20
Add some missing smallcaps.
Théo Zimmermann
2020-10-12
Add missing ";" in record grammar
Jim Fehrle
2020-05-14
Add some markers of origin.
Théo Zimmermann
2020-05-14
Reintroduce leftover parts; update index files; small fixes.
Théo Zimmermann
2020-05-13
Merge section on Inductive types from Gallina and CIC.
Théo Zimmermann
2020-05-13
Create new file on Inductive types.
Théo Zimmermann
2020-05-13
Merge sections on Inductive types and Recursive functions in new file.
Théo Zimmermann
2020-05-13
Add Recursive functions to new file on Inductive types.
Théo Zimmermann
2020-05-13
Create new file on Inductive types.
Théo Zimmermann