diff options
Diffstat (limited to 'doc/refman/Classes.tex')
| -rw-r--r-- | doc/refman/Classes.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 069b99127..e8ebb9f99 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -107,7 +107,7 @@ satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be found, an error is raised: \begin{coq_example} -Definition neqb' (A : Type) (x y : A) := negb (eqb x y). +Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y). \end{coq_example} The algorithm used to solve constraints is a variant of the eauto tactic |