diff options
Diffstat (limited to 'ide/interface.mli')
| -rw-r--r-- | ide/interface.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/interface.mli b/ide/interface.mli index 77a875b7d2..cbaa027508 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -200,7 +200,7 @@ type init_rty = state_id type about_sty = unit type about_rty = coq_info -type handle_exn_sty = exn +type handle_exn_sty = Exninfo.iexn type handle_exn_rty = state_id * location * string (* Retrocompatibility stuff *) |