doc/sphinx/language/core · coq · Tangled

forked from coq/coq

coq doc sphinx language core

13 files

coqbot-app[bot] · Merge PR #22614: printing: warn when module contents cannot be printed · 3w ago

assumptions.rst

Doc: add missing names of warnings

Doc: add missing names of warnings

coinductive.rst

Doc: rename `coqtop::` -> `rocqtop::`, `coqdoc::` -> `rocqdoc::`

Warning for missing "Proof" command and error on duplicate or late "Proof"

definitions.rst

Doc: add crosslink between Definition and Eval and index entry "Eval (Definition)"

Move Proof Mode and SSR chapter one level up.

Warning for missing "Proof" command and error on duplicate or late "Proof"

Merge PR #22614: printing: warn when module contents cannot be printed

Document undocumented options

Doc: add missing names of warnings

Deprecate Notation for Abbreviation

Update doc for Type -> Univ change a bit

Use levels for associativity in refman