diff options
Diffstat (limited to 'toplevel/whelp.ml4')
| -rw-r--r-- | toplevel/whelp.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index aa38e9e9f..332d30536 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -10,7 +10,7 @@ open Flags open Pp -open Util +open Errors open System open Names open Term |