diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-28 16:35:13 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-28 16:35:13 +0200 |
| commit | 064481e3d00f4b8d1572b5f6e90a5f1c74cc6946 (patch) | |
| tree | 745650ad339cdfe5baf573817a4b3da605f84659 /doc | |
| parent | c7e78c3b66eabeb0646feabfd38204209e5a2fa2 (diff) | |
Chapter 1 of the refman compiles without reporting any undocumented object.
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) |