From 3a7d9fcafedc4987d0748a8717b2b012a779de39 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 16 Feb 2017 14:14:34 +0100 Subject: [stm] Remove edit_id. We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203. --- kernel/term_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 6dfa64357..88a4fa529 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -194,7 +194,7 @@ let rec unzip ctx j = let feedback_completion_typecheck = let open Feedback in Option.iter (fun state_id -> - feedback ~id:(State state_id) Feedback.Complete) + feedback ~id:state_id Feedback.Complete) let infer_declaration ~trust env kn dcl = match dcl with -- cgit v1.2.3