diff options
Diffstat (limited to 'checker/include')
-rw-r--r-- | checker/include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/include b/checker/include index f5bd2984..6bea3c91 100644 --- a/checker/include +++ b/checker/include @@ -31,7 +31,7 @@ open Typeops;; open Check;; open Pp;; -open Errors;; +open CErrors;; open Util;; open Names;; open Term;; |