Index of exceptions

A
AmbiguousPath [Env]
Arg_error [Args_wrapper]
Arg_expected [Args_wrapper]
Arg_expected_none [Args_wrapper]
Arg_parse_type_error [Args_wrapper]
Arg_pr_not_found [Args_wrapper]
Arg_qid_not_found [Args_wrapper]
Arg_theory_not_found [Args_wrapper]
AssignPrivate [Ity]
AssignSnapshot [Ity]
B
BadArity [Term]
BadConstructor [Decl]
BadCopyPaste [Controller_itp.Make]
BadFloatSpec [Ty]
BadGhostWrite [Ity]
BadID [Session_itp]
BadInstance [Theory]
BadItyArity [Ity]
BadLogicDecl [Decl]
BadMetaArity [Theory]
BadRecordField [Decl]
BadRegArity [Ity]
BadTypeArity [Ty]
Bad_name_table [Trans]
BoolExpected [Rc]

BoolExpected key value bool expected

C
CannotInstantiate [Theory]
CannotOpen [Rc]
ClashIdent [Decl]
ClashSymbol [Theory]
CloseTheory [Theory]
ConfigFailure [Whyconf]
ConstructorExpected [Expr]
ConstructorExpected [Term]
D
DuplicateField [Ity]
DuplicateField [Rc]

DuplicateField key key key appears more than once

DuplicateRecordField [Decl]
DuplicateRegion [Ity]
DuplicateSection [Rc]

DuplicateSection name section name appears more than once

DuplicateShortcut [Whyconf]
DuplicateTypeVar [Ty]
DuplicateVar [Term]
E
EmptyAlgDecl [Decl]
EmptyCase [Term]
EmptyDecl [Decl]
EmptyIndDecl [Decl]
EmptyRange [Ty]
EmptyRecord [Decl]
Errors_list [Controller_itp]
ExceptionLeak [Expr]
ExtraParameters [Rc]

ExtraParameters name One section of name name has two many parameters : more than one if name is a family, more than none if name is a section

F
FieldExpected [Expr]
FloatConflict [Theory]
FmlaExpected [Term]
FoldSkip [Util]
FunctionSymbolExpected [Term]
G
GhostDivergence [Ity]
GoalFound [Task]
GoalNotFound [Task]
I
IllegalAlias [Ity]
IllegalAssign [Ity]
IllegalFlagTrans [Trans]
IllegalSnapshot [Ity]
IllegalTypeAlias [Decl]
IllegalTypeParameters [Ty]
IllegalUpdate [Ity]
ImpureVariable [Ity]
IncompatibleNotation [Pmodule]
IntExpected [Rc]

IntExpected key value int expected

InvalidConstantLiteral [Number]
InvalidFormat [Env]
InvalidIndDecl [Decl]
InvalidIntegerLiteralType [Term]
InvalidRealLiteralType [Term]
K
KnownFormat [Env]
KnownIdent [Decl]
KnownMeta [Theory]
KnownTrans [Trans]
L
LemmaFound [Task]
LibraryConflict [Env]
LibraryNotFound [Env]
Located [Loc]
M
Message [Loc]
MetaTypeMismatch [Theory]
MissingField [Rc]

MissingField key The field key is required but not given

MissingParameters [Rc]

MissingParameters name One section of a family name has no parameters

ModuleNotFound [Pmodule]
N
NoOpenedNamespace [Theory]
NoProgress [Session_itp]
NoTerminationProof [Decl]
NonFoundedTypeDecl [Decl]
NonLocal [Theory]
NonPositiveIndDecl [Decl]
NonPositiveTypeDecl [Decl]
NonRepresentableFloat [Number]
NotExclusiveMeta [Task]
NotImplemented [Printer]
NotTaggingMeta [Task]
O
OutOfRange [Number]
P
ParseFilterProver [Whyconf]
Parse_error [Args_wrapper]
PredicateSymbolExpected [Term]
ProverAmbiguity [Whyconf]
ProverNotFound [Whyconf]
R
RangeConflict [Theory]
RecordFieldMissing [Decl]
RedeclaredIdent [Decl]
RemoveError [Session_itp]
S
StaleVariable [Ity]
StringExpected [Rc]

StringExpected key value string expected

SyntaxErrorFile [Rc]
T
TermExpected [Term]
TheoryNotFound [Env]
TransAlreadyExists [Controller_itp.Make]
TransFailure [Trans]
TypeMismatch [Ity]
TypeMismatch [Ty]
U
UnboundRegion [Ity]
UnboundTypeVar [Ty]
UnboundVar [Decl]
UncoveredVar [Term]
UnexpectedProp [Ty]
UnknownExtension [Env]
UnknownField [Rc]

UnknownField key The key key appeared in a section but is not expected there

UnknownFlagTrans [Trans]
UnknownFormat [Env]
UnknownIdent [Decl]
UnknownMeta [Theory]
UnknownTrans [Trans]
Unnecessary_arguments [Args_wrapper]
UnspecifiedFormat [Env]
Unsupported [Printer]

This exception must be raised only inside a call of one of the catch_* functions below

UnsupportedDecl [Printer]
UnsupportedTerm [Printer]
UnsupportedType [Printer]
W
WriteImmutable [Ity]