From 90ae0897e80106194795e179d580da0d1118aaf2 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 09:14:23 +0100
Subject: CLEANUP PROPOSITION: s/local context of parameters/context of
 parameters

---
 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 adaa20de86..6f0e952ce6 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1055,7 +1055,7 @@ The following typing rule is added to the theory.
 \begin{description}
 \item[Ind-Family] Let $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ be an
   inductive definition. Let $\Gamma_P = [p_1:P_1;\ldots;p_{p}:P_{p}]$
-  be its local context of parameters, $\Gamma_I = [I_1:\forall
+  be its context of parameters, $\Gamma_I = [I_1:\forall
     \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ its context of
   definitions and $\Gamma_C = [c_1:\forall
     \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$ its context of
-- 
cgit v1.2.3