\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \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}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \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{\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 or tactics¶

You may use the following attribute to deprecate a notation or tactic. 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.

This attribute is supported by the following commands: Ltac, Tactic Notation, Notation, Infix, Ltac2, Ltac2 Notation, Ltac2 external.

It can trigger the following warnings:

Warning Tactic qualid is deprecated since string_since. string_note.¶
Warning Tactic Notation qualid is deprecated since string_since. string_note.¶
Warning Notation string is deprecated since string_since. string_note.¶
Warning Ltac2 definition qualid is deprecated since string_since. string_note.¶
Warning Ltac2 alias qualid is deprecated since string_since. string_note.¶
Warning Ltac2 notation ltac2_scope+ is deprecated since string_since. string_note.¶: qualid or string is the notation, string_since is the version number, string_note is the note (usually explains the replacement).

Example: Deprecating a tactic.

#[deprecated(since="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 0.9. Use idtac instead. [deprecated-tactic,deprecated] 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="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 1.2. Use bar instead. [deprecated-syntactic-definition,deprecated] bar 0 : nat