diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml index 83e318fce..6dbede402 100644 --- a/controller-js/coq_lsp_worker.ml +++ b/controller-js/coq_lsp_worker.ml @@ -81,9 +81,7 @@ let setup_std_printers () = external coq_vm_trap : unit -> unit = "coq_vm_trap" -let post_message (json : Yojson.Safe.t) = - let js = json_to_obj (Js.Unsafe.obj [||]) json in - Worker.post_message js +let post_message (json : Yojson.Safe.t) = let js = json_to_obj (Js.Unsafe.obj [||]) json in Worker.post_message js external interrupt_setup : opaque (* Uint32Array *) -> unit = "interrupt_setup" diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index ab3cdf063..f02ace76a 100644 --- a/editor/code/lib/types.ts +++ b/editor/code/lib/types.ts @@ -30,9 +30,7 @@ export interface Message { } export interface GoalAnswer { - textDocument: VersionedTextDocumentIdentifier; - position: Position; - goals?: GoalConfig; + textDocument: VersionedTextDocumentIdentifier; position: Position; goals?: GoalConfig; messages: Pp[] | Message[]; error?: Pp; }