diff options
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 3a834ff8a..5dc06f33c 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1192,8 +1192,6 @@ Check (fun l:list (list nat) => map length l). \Rem To know which are the implicit arguments of an object, use the command {\tt Print Implicit} (see \ref{PrintImplicit}). -\Rem - \Rem If the list of arguments is empty, the command removes the implicit arguments of {\qualid}. |