From 064481e3d00f4b8d1572b5f6e90a5f1c74cc6946 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 28 May 2018 16:35:13 +0200 Subject: Chapter 1 of the refman compiles without reporting any undocumented object. --- doc/sphinx/language/gallina-specification-language.rst | 1 + 1 file changed, 1 insertion(+) (limited to 'doc') 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) -- cgit v1.2.3