\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Writing Coq libraries and plugins

This section presents the part of the Coq language that is useful only to library and plugin authors. A tutorial for writing Coq plugins is available in the Coq repository in doc/plugin_tutorial.

Deprecating library objects, tactics or library files

You may use the following attribute to deprecate a notation, tactic, definition, axiom, theorem or file. When renaming a definition or theorem, you can introduce a deprecated compatibility alias using Notation (abbreviation) (see the example below).

Attribute deprecated ( since = string ,? note = string? )

At least one of since or note must be present. If both are present, either one may appear first and they must be separated by a comma. If they are present, they will be used in the warning message, and since will also be used in the warning name and categories.

This attribute is supported by the following commands: Ltac, Tactic Notation, Notation, Infix, Ltac2, Ltac2 Notation, Ltac2 external, Definition, Theorem, and similar commands. To attach it to a compiled library file, use Attributes.

It can trigger the following warnings:

Warning Library File qualid is deprecated since string_since. string_note

Warning Library File (transitively required) qualid is deprecated since string_since. string_note

Warning Ltac2 alias qualid is deprecated since string_since. string_note

Warning Ltac2 definition qualid is deprecated since string_since. string_note

Warning Ltac2 notation ltac2_scope+ is deprecated since string_since. string_note

Warning Notation string is deprecated since string_since. string_note

Warning Tactic qualid is deprecated since string_since. string_note

Warning Tactic Notation qualid is deprecated since string_since. string_note

qualid or string is the notation, stringsince is the version number, stringnote is the note (usually explains the replacement).

Explicitly Requireing a file that has been deprecated, using the Attributes command, triggers a Library File deprecation warning. Requiring a deprecated file, even indirectly through a chain of Requires, will produce a Library File (transitively required) deprecation warning if the Warnings option "deprecated-transitive-library-file" is set (it is "-deprecated-transitive-library-file" by default, silencing the warning).

Note

Coq and its standard library follow this deprecation policy:

• it should always be possible for a project written in Coq to be compatible with two successive major versions,

• features must be deprecated in one major version before removal,

• Coq developers should provide an estimate of the required effort to fix a project with respect to a given change,

• breaking changes should be clearly documented in the public release notes, along with recommendations on how to fix a project if it breaks.

See [Zim19], Section 3.6.3, for more details.

Example: Deprecating a tactic.

#[deprecated(since="mylib 0.9", note="Use idtac instead.")] Ltac foo := idtac.

foo is defined

Goal True.

1 goal ============================ True

Proof.

now foo.

Toplevel input, characters 4-7: > now foo. > ^^^ Warning: Tactic foo is deprecated since mylib 0.9. Use idtac instead. [deprecated-tactic-since-mylib-0.9,deprecated-since-mylib-0.9,deprecated-tactic,deprecated,default] No more goals.

Example: Introducing a compatibility alias

Let's say your library initially contained:

Definition foo x := S x.

foo is defined

and you want to rename foo into bar, but you want to avoid breaking your users' code without advanced notice. To do so, replace the previous code by the following:

Definition bar x := S x.

bar is defined

#[deprecated(since="mylib 1.2", note="Use bar instead.")] Notation foo := bar (only parsing).

Then, the following code still works, but emits a warning:

Check (foo 0).

Toplevel input, characters 7-10: > Check (foo 0). > ^^^ Warning: Notation foo is deprecated since mylib 1.2. Use bar instead. [deprecated-syntactic-definition-since-mylib-1.2,deprecated-since-mylib-1.2,deprecated-syntactic-definition,deprecated,default] bar 0 : nat