| ClashType of string |
| ClashLabel of string * string |
| ClashParam of string |
| TypeDuplicateVar of string |
| UnboundedVar of string |
| UnknownType of string |
| WrongArity of string * int |
| SymbAlreadyDefined of string |
| SymbUndefined of string |
| NotAPropVar of string |
| NotAPredicate of string |
| Unification of Ty.t * Ty.t |
| ShouldBeApply of string |
| WrongNumberofArgs of string |
| ShouldHaveType of Ty.t * Ty.t |
| ShouldHaveTypeIntorReal of Ty.t |
| ShouldHaveTypeInt of Ty.t |
| ShouldHaveTypeBitv of Ty.t |
| ArrayIndexShouldHaveTypeInt |
| ShouldHaveTypeArray |
| ShouldHaveTypeRecord of Ty.t |
| ShouldBeARecord |
| ShouldHaveLabel of string * string |
| NoLabelInType of Hstring.t * Ty.t |
| ShouldHaveTypeProp |
| NoRecordType of Hstring.t |
| DuplicateLabel of Hstring.t |
| DuplicatePattern of string |
| WrongLabel of Hstring.t * Ty.t |
| WrongNumberOfLabels |
| Notrigger |
| CannotGeneralize |
| SyntaxError |
| ThExtError of string |
| ThSemTriggerError |
| WrongDeclInTheory |
| ShouldBeADT of Ty.t |
| MatchNotExhaustive of Hstring.t list |
| MatchUnusedCases of Hstring.t list |
| NotAdtConstr of string * Ty.t |