diff options
Diffstat (limited to 'doc/refman/Natural.tex')
| -rw-r--r-- | doc/refman/Natural.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex index 9a9abe5df..f33c0d356 100644 --- a/doc/refman/Natural.tex +++ b/doc/refman/Natural.tex @@ -158,7 +158,7 @@ Add Natural Implicit constr1. By default, the proposition (or predicate) constructors \verb=conj=, \verb=or_introl=, \verb=or_intror=, \verb=ex_intro=, -\verb=exT_intro=, \verb=refl_equal=, \verb=refl_eqT= and \verb=exist= +\verb=eq_refl= and \verb=exist= \noindent are declared implicit. Note that declaring implicit the constructor of a datatype (i.e. an inductive type of type \verb=Set=) |