aboutsummaryrefslogtreecommitdiff
path: root/ide/interface.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/interface.mli')
-rw-r--r--ide/interface.mli6
1 files changed, 4 insertions, 2 deletions
diff --git a/ide/interface.mli b/ide/interface.mli
index 9ed6062588..62f63aefb9 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -111,8 +111,10 @@ type coq_info = {
(** Calls result *)
type location = (int * int) option (* start and end of the error *)
-type state_id = Feedback.state_id
-type edit_id = Feedback.edit_id
+type state_id = Stateid.t
+
+(* Obsolete *)
+type edit_id = int
(* The fail case carries the current state_id of the prover, the GUI
should probably retract to that point *)