Index of exceptions

A
AmbiguousPath [Env]
ArrowExpected [Mlw_expr]
B
BadArity [Term]
BadConstructor [Decl]
BadFloatSpec [Ty]
BadInstance [Theory]
BadItyArity [Mlw_ty]
BadLogicDecl [Decl]
BadMetaArity [Theory]
BadRecordField [Decl]
BadRegArity [Mlw_ty]
BadTypeArity [Ty]
BoolExpected [Rc]

BoolExpected key value bool expected

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

DuplicateField key key key appears more than once

DuplicateRecordField [Decl]
DuplicateRegion [Mlw_ty]
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]
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
FmlaExpected [Term]
FoldSkip [Util]
FunctionSymbolExpected [Term]
G
GhostDiverg [Mlw_ty]
GoalFound [Task]
GoalNotFound [Task]
H
HiddenPLS [Mlw_expr]
I
IllegalAlias [Mlw_ty]
IllegalCompar [Mlw_ty]
IllegalTypeAlias [Decl]
IllegalTypeParameters [Ty]
Immutable [Mlw_expr]
IntExpected [Rc]

IntExpected key value int expected

InvalidFormat [Env]
InvalidIndDecl [Decl]
InvalidIntegerLiteralType [Term]
InvalidRealLiteralType [Term]
K
KnownFormat [Env]
KnownIdent [Decl]
KnownMeta [Theory]
L
LemmaFound [Task]
LibraryConflict [Env]
LibraryNotFound [Env]
M
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 [Mlw_module]
ModuleOrTheoryNotFound [Mlw_module]
MutableException [Mlw_ty]
N
NoOpenedNamespace [Theory]
NoTask [Session]
NoTerminationProof [Decl]
NonFoundedTypeDecl [Decl]
NonLocal [Theory]
NonPositiveIndDecl [Decl]
NonPositiveTypeDecl [Decl]
NonupdatableType [Mlw_decl]
NotExclusiveMeta [Task]
NotTaggingMeta [Task]
O
OutdatedSession [Session]
P
ParseFilterProver [Whyconf]
PolymorphicException [Mlw_ty]
PredicateSymbolExpected [Term]
ProverAmbiguity [Whyconf]
ProverNotFound [Whyconf]
R
RdOnlyPLS [Mlw_expr]
RecordFieldMissing [Decl]
RedeclaredIdent [Decl]
RegionMismatch [Mlw_ty]
S
SessionFileError [Session]
ShapesFileError [Session]
SkipFound [Task]
StaleRegion [Mlw_expr]

freshness violation: a previously reset region is associated to an ident

StringExpected [Rc]

StringExpected key value string expected

SyntaxErrorFile [Rc]
T
TermExpected [Term]
TheoryNotFound [Env]
TooLateInvariant [Mlw_module]
TypeMismatch [Mlw_ty]
TypeMismatch [Ty]
U
UnboundException [Mlw_ty]

every raised exception must have a postcondition in spec.c_xpost

UnboundRegion [Mlw_ty]
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

UnknownFormat [Env]
UnknownIdent [Decl]
UnknownMeta [Theory]
UnspecifiedFormat [Env]
V
ValueExpected [Mlw_expr]