aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/Setoid.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index b124d6a969..a5cc6acbf0 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -454,9 +454,9 @@ is equivalent to an instance declaration:
\texttt{Instance} ($x_1 : T_1$) \ldots ($x_n : T_k$) \texttt{=>}
\textit{id} : \texttt{Equivalence} \textit{(A $t_1$ \ldots $t_n$) (Aeq
$t'_1$ \ldots $t'_m$)} :=\\
- ~\zeroone{\texttt{equiv\_refl :=} \textit{refl}}\\
- ~\zeroone{\texttt{equiv\_sym :=} \textit{sym}}\\
- ~\zeroone{\texttt{equiv\_trans :=} \textit{trans}}.
+ ~\zeroone{\texttt{equivalence\_reflexive :=} \textit{refl}}\\
+ ~\zeroone{\texttt{equivalence\_symmetric :=} \textit{sym}}\\
+ ~\zeroone{\texttt{equivalence\_transitive :=} \textit{trans}}.
\end{quote}
The declaration itself amounts to the definition of an object of the