From 8efc7854332a3376a0e7ec348545cff83829a70e Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 6 Nov 2015 14:36:38 +0100
Subject: CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive
 definition.

---
 doc/refman/RefMan-cic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index db80d79109..1cb0a7318e 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1622,7 +1622,7 @@ following typing rule
 (\WTEG{f_i}{\CI{(c_{p_i}~q_1\ldots  q_r)}{P}})_{i=1\ldots  l}}
 {\WTEG{\Case{P}{c}{f_1|\ldots  |f_l}}{(P\ t_1\ldots  t_s\ c)}}}%\\[3mm]
 
-provided $I$ is an inductive type in a declaration
+provided $I$ is an inductive type in a definition
 \Ind{}{r}{\Gamma_I}{\Gamma_C} with 
 $\Gamma_C = [c_1:C_1;\ldots;c_n:C_n]$ and $c_{p_1}\ldots  c_{p_l}$ are the
 only constructors of $I$.
-- 
cgit v1.2.3