aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.mli')
-rw-r--r--toplevel/coqloop.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 4aedaa035..3011471f2 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -30,7 +30,7 @@ val set_prompt : (unit -> string) -> unit
May raise only the following exceptions: [Drop] and [End_of_input],
meaning we get out of the Coq loop. *)
-val print_toplevel_error : exn -> std_ppcmds
+val print_toplevel_error : Exninfo.iexn -> std_ppcmds
(** Parse and execute one vernac command. *)