diff options
| author | Pierre-Marie Pédrot | 2015-09-13 17:19:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-20 15:20:32 +0200 |
| commit | 002cd2e8f6ae5722e72a5db136cda7414f9218d5 (patch) | |
| tree | e45f8de4e5c493f08a5cabf4593125f4befe66fb /ide/interface.mli | |
| parent | f20fce1259563f2081fadc62ccab1304bb8161d5 (diff) | |
Rich printing of CoqIDE protocol failure.
Diffstat (limited to 'ide/interface.mli')
| -rw-r--r-- | ide/interface.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/interface.mli b/ide/interface.mli index 848fb817d4..f3777ba36c 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -118,7 +118,7 @@ type edit_id = Feedback.edit_id should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * string) + | Fail of (state_id * location * richpp) type ('a, 'b) union = ('a, 'b) Util.union @@ -202,7 +202,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * string +type handle_exn_rty = state_id * location * richpp (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string |