From 55fee343ecbb6e510aa9c2729627fe7a758f384b Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 16:31:57 +0100
Subject: CLEANUP: originally, we talked about "B" as an "arity"

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 9cb52dba28..5a8dcfc245 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1372,7 +1372,7 @@ definitions.
 We define now a relation \compat{I:A}{B} between an inductive
 definition $I$ of type $A$ and an arity $B$. This relation states that
 an object in the inductive definition $I$ can be eliminated for
-proving a property $\lb a x \mto P$ of type $B$.
+proving a property $\lb a x \mto P$ of arity $B$.
 % QUESTION: Is it necessary to explain the meaning of [I:A|B] in such a complicated way?
 % Couldn't we just say that: "relation [I:A|B] defines which types can we choose as 'result types'
 % with respect to the type of the matched object".
-- 
cgit v1.2.3