From f7051cd4eb4cefc4b2ec04c8c29369dcaf0062f2 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 6 Nov 2015 15:18:35 +0100
Subject: ENH: define the meaning of 'p'

---
 doc/refman/RefMan-cic.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 87ef046fa4..91c1418546 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1571,7 +1571,7 @@ elimination on any sort is allowed.
 Let $c$ be a term of type $C$, we assume $C$ is a type of constructor
 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.
+We assume $r$ is the number of parameters and $p$ is the number of arguments.
 
 We define a new type \CI{c:C}{P} which represents the type of the
 branch corresponding to the $c:C$ constructor.
@@ -1584,7 +1584,7 @@ branch corresponding to the $c:C$ constructor.
 We write \CI{c}{P} for \CI{c:C}{P} with $C$ the type of $c$.
 
 \paragraph{Examples.}
-For $\ListA$ the type of $P$ will be $\ListA\ra s$ for $s \in \Sort$. \\ 
+For $\List \nat$ the type of $P$ will be $\ListA\ra s$ for $s \in \Sort$. \\ 
 $ \CI{(\cons~A)}{P} \equiv
 \forall a:A, \forall l:\ListA,(P~(\cons~A~a~l))$.
 
-- 
cgit v1.2.3