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
/
basic.rst
Age
Commit message (
Collapse
)
Author
2020-06-09
Minor improvements to the section on basics.
Théo Zimmermann
2020-06-08
Convert Ltac chapter to prodn
Jim Fehrle
2020-05-27
Changelog entries for the 8.12 changes to the reference manual.
Théo Zimmermann
2020-05-18
Use the new gdef alt-text feature in the refman.
Théo Zimmermann
2020-05-15
Merge PR #11948: Hexadecimal numerals
Hugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-09
[doc] Add hexadecimal numerals
Pierre Roux
2020-05-06
Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann.
Hugo Herbelin
2020-05-06
Documenting plugin/tactic/stdlib keywords in corresponding chapters.
Hugo Herbelin
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from keywords. It is enough to make them normal identifiers. Note: - keywords reserved by the tactics are: ** [= _eqn |- by using - keywords reserved by ltac are: lazymatch multimatch ||
2020-05-01
Move essential vocabulary and syntax conventions to section on basics.
Théo Zimmermann
2020-05-01
Create basics out of sections from Gallina and Vernac chapters.
Théo Zimmermann
2020-05-01
Create section on basics with just flags, options and tables.
Théo Zimmermann
2020-05-01
Create section on basics with just lexical conventions and attributes.
Théo Zimmermann
