diff options
Diffstat (limited to 'doc/RefMan-cic.tex')
| -rwxr-xr-x | doc/RefMan-cic.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex index 483fedbb87..4fd12e0f2d 100755 --- a/doc/RefMan-cic.tex +++ b/doc/RefMan-cic.tex @@ -579,8 +579,8 @@ $\Gamma_C$. The occurrences of the variables of $\Gamma_P$ in the contexts $\Gamma_I$ and $\Gamma_C$ are bound. -The definition \Ind{\Gamma}{\Gamma_P}{\;\Gamma_I}{\Gamma_C\;} will be -well-formed exactly when \NInd{\Gamma,\Gamma_P}{\;\Gamma_I}{\Gamma_C\;} is. +The definition \Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} will be +well-formed exactly when \NInd{\Gamma,\Gamma_P}{\Gamma_I}{\Gamma_C} is. If $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$, an object in \Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} applied to $q_1,\ldots,q_r$ will behave as the corresponding object of |