aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/cerrors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/cerrors.mli')
-rw-r--r--toplevel/cerrors.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 2207608a8..1703a072d 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -10,11 +10,12 @@
(*i*)
open Pp
+open Util
(*i*)
(* Error report. *)
-val print_loc : Coqast.loc -> std_ppcmds
+val print_loc : loc -> std_ppcmds
val explain_exn : exn -> std_ppcmds