16.4 Error messages
16.4 Error messages
An error occurs when trying to Print, to Add, to
Test, or to remove an undefined ident. Similarly, an
error occurs when trying to set a language unknown from Natural.
Errors may also occur when trying to parametrize the printing of
proofs: some parametrization are effectively forbidden.
Note that to Remove an ident absent from a table or to
Add to a table an already present ident does not lead to an
error.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.5.3.html at 8/10/98