From b090f65cf35e45596c10a7513bb3e8058069e4fd Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Thu, 31 Jan 2019 15:54:57 +0900
Subject: Remove "End TreeExample." line.

This corresponds to "Module TreeExample." removed at
2018-04-24 bcf5352cc7a26a672e719f7dad4021c69d723833.
---
 doc/sphinx/language/cic.rst | 1 -
 1 file changed, 1 deletion(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 25a230015c..6ddfe14eea 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -930,7 +930,6 @@ condition* for a constant :math:`X` in the following cases:
       Inductive nattree (A:Type) : Type :=
       | leaf : nattree A
       | node : A -> (nat -> nattree A) -> nattree A.
-      End TreeExample.
 
    Then every instantiated constructor of ``nattree A`` satisfies the nested positivity
    condition for ``nattree``:
-- 
cgit v1.2.3