doc/sphinx/addendum · coq · Tangled

forked from coq/coq

coq doc sphinx addendum

15 files

Gaëtan Gilbert · Doc: add missing names of warnings · 3w ago

canonical-structures.rst

Add redirects for HTML pages that were moved.

extended-pattern-matching.rst

Add redirects for HTML pages that were moved.

Extraction: allow plugins to add extraction languages

generalized-rewriting.rst

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

implicit-coercions.rst

Doc: add missing names of warnings

doc: add missing option values

miscellaneous-extensions.rst

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

Add documentation for ensatz tactic.

parallel-proof-processing.rst

Update parallel-proof-processing.rst

Optionally warn on admitted proofs.

rewrite-rules.rst

Revert name change of univ_decl to sort_poly_decl

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

Doc: add missing names of warnings

type-classes.rst

Doc: add missing names of warnings

universe-polymorphism.rst

Doc: add missing names of warnings