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
(see the example below).
deprecated ( since = string ,? note = string? )¶
At least one of
notemust be present. If both are present, either one may appear first and they must be separated by a comma.
It can trigger the following warnings:
Tactic qualid is deprecated since stringsince. stringnote.¶
Tactic Notation qualid is deprecated since stringsince. stringnote.¶
Notation string is deprecated since stringsince. stringnote.¶
Example: Deprecating a tactic.
- #[deprecated(since="0.9", note="Use idtac instead.")] Ltac foo := idtac.
- foo is defined
- Goal True.
- 1 goal ============================ True
- 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
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