diff options
Diffstat (limited to 'docs/opt-coercion/fc-normalization-rta.tex')
| -rwxr-xr-x | docs/opt-coercion/fc-normalization-rta.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/opt-coercion/fc-normalization-rta.tex b/docs/opt-coercion/fc-normalization-rta.tex index 0600427e98..942dcefbf4 100755 --- a/docs/opt-coercion/fc-normalization-rta.tex +++ b/docs/opt-coercion/fc-normalization-rta.tex @@ -1184,7 +1184,7 @@ impressive simplifications from Section~\ref{ssect:large}. Consider that example Notably, rules \rulename{AxSuckL/R} and \rulename{SymAxSuckL/R} generate axiom applications of the form $C\;\gammas$ (with a coercion as argument). In our previous papers, the syntax of axiom applications was $C\;\taus$, with \emph{types} -as arugments. But we need the additional generality to allow coercions rewriting to +as arguments. But we need the additional generality to allow coercions rewriting to proceed without getting stuck. %% which we now give in mathematical notation. The |