diff options
| author | Maxime Dénès | 2017-06-20 10:47:40 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-20 10:47:40 +0200 |
| commit | 9c5378131c90c7fb819743d8e79c226492a0331f (patch) | |
| tree | 444f14b11613ebd90d7a9d154cd484f6624b6753 /ide/interface.mli | |
| parent | 6cae6006a95ca7587180a1293ab41d48877e79ea (diff) | |
| parent | d8874dd855d748aaaf504890487ab15ffd7a677d (diff) | |
Merge PR#774: [ide] Add route_id parameter to query call.
Diffstat (limited to 'ide/interface.mli')
| -rw-r--r-- | ide/interface.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/ide/interface.mli b/ide/interface.mli index 62f63aefb9..1a4d6c0ecb 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -112,6 +112,7 @@ type coq_info = { type location = (int * int) option (* start and end of the error *) type state_id = Stateid.t +type route_id = Feedback.route_id (* Obsolete *) type edit_id = int @@ -154,8 +155,8 @@ type edit_at_rty = (unit, state_id * (state_id * state_id)) union has been deprecated in favor of sending the query answers as feedback. It will be removed in a future version of the protocol. *) -type query_sty = string * state_id -type query_rty = string +type query_sty = route_id * (string * state_id) +type query_rty = unit (** Fetching the list of current goals. Return [None] if no proof is in progress, [Some gl] otherwise. *) |