diff options
Diffstat (limited to 'lib/util.ml')
| -rw-r--r-- | lib/util.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/lib/util.ml b/lib/util.ml index 242c203211..5cd351237f 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -19,8 +19,6 @@ exception UserError of string * std_ppcmds (* User errors *) let error string = raise (UserError(string, str string)) let errorlabstrm l pps = raise (UserError(l,pps)) -exception AnomalyOnError of string * exn - exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *) let alreadydeclared pps = raise (AlreadyDeclared(pps)) |