diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 9f154b89a..7c3dc2a14 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1248,6 +1248,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: the theorem is bound to the name :token:`ident` in the environment. .. exn:: The term @term has type @type which should be Set, Prop or Type. + :undocumented: .. exn:: @ident already exists. :name: @ident already exists. (Theorem) |