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]
InvalidLiteralType [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]