diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-05 09:14:23 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:15 +0100 |
| commit | 90ae0897e80106194795e179d580da0d1118aaf2 (patch) | |
| tree | d69db61c0ed806189ec1cd8bd94b1472b883a585 /doc/refman/RefMan-cic.tex | |
| parent | 1a51c868d6f342c094f2d9f0b8101d6c13720537 (diff) | |
CLEANUP PROPOSITION: s/local context of parameters/context of parameters
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index adaa20de8..6f0e952ce 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 |