From 38fc8566ab59bcf67e6eeaf5860ce97cfab38e74 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 6 Nov 2015 15:09:34 +0100
Subject: CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive
 definition'? Doesn't make more sense to refer to it as 'inductive type'?

---
 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 1cb0a7318e..87ef046fa4 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1569,7 +1569,7 @@ elimination on any sort is allowed.
 
 \paragraph{Type of branches.}
 Let $c$ be a term of type $C$, we assume $C$ is a type of constructor
-for an inductive definition $I$. Let $P$ be a term that represents the
+for an inductive type $I$. Let $P$ be a term that represents the
 property to be proved.
 We assume $r$ is the number of parameters.
 
-- 
cgit v1.2.3