diff --git a/CHANGES.md b/CHANGES.md
index 93b4e560..00a2858a 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -36,6 +36,8 @@
    see some motivation for that (@ejgallego, #841)
  - [lsp] [diagnostics] (! breaking change) change type of diagnostics
    extra data from list to named record (@ejgallego, #843)
+ - [lsp] Implement support for `textDocument/codeAction`. For now, we
+   support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845)
 
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------
diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml
index eb33483e..5479d96e 100644
--- a/controller/lsp_core.ml
+++ b/controller/lsp_core.ml
@@ -416,6 +416,20 @@ let do_document = do_document_request_maybe ~handler:Rq_document.request
 let do_save_vo = do_document_request_maybe ~handler:Rq_save.request
 let do_lens = do_document_request_maybe ~handler:Rq_lens.request
 
+(* could be smarter *)
+let do_action ~params =
+  let range = field "range" params in
+  match Lsp.JLang.Diagnostic.Range.of_yojson range with
+  | Ok range ->
+    let range = Lsp.JLang.Diagnostic.Range.vnoc range in
+    do_immediate ~params ~handler:(Rq_action.request ~range)
+  | Error err ->
+    (* XXX: We really need to fix the parsing error handling in lsp_core, we got
+       it right in petanque haha *)
+    (* JSON-RPC Parse error (EJGA: is this the right code) *)
+    let code = -32700 in
+    Rq.Action.error (code, err)
+
 let do_cancel ~ofn_rq ~params =
   let id = int_field "id" params in
   let code = -32800 in
@@ -584,6 +598,7 @@ let dispatch_request ~token ~method_ ~params : Rq.Action.t =
   | "textDocument/hover" -> do_hover ~params
   | "textDocument/codeLens" -> do_lens ~params
   | "textDocument/selectionRange" -> do_selectionRange ~params
+  | "textDocument/codeAction" -> do_action ~params
   (* Proof-specific stuff *)
   | "proof/goals" -> do_goals ~params
   (* Proof-specific stuff *)
diff --git a/controller/rq_action.ml b/controller/rq_action.ml
new file mode 100644
index 00000000..8e956399
--- /dev/null
+++ b/controller/rq_action.ml
@@ -0,0 +1,65 @@
+let point_lt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ }
+    { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } =
+  l1 < l2 || (l1 = l2 && c1 < c2)
+
+let point_gt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ }
+    { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } =
+  l1 > l2 || (l1 = l2 && c1 > c2)
+
+(* To move to doc.ml *)
+let filter_map_range ~range ~nodes ~f =
+  let rec aux (nodes : Fleche.Doc.Node.t list) acc =
+    match nodes with
+    | [] -> List.rev acc
+    | node :: nodes -> (
+      let open Lang.Range in
+      let nrange = node.range in
+      if point_lt nrange.end_ range.start then aux nodes acc
+      else if point_gt nrange.start range.end_ then List.rev acc
+      else
+        (* Node in scope *)
+        match f node with
+        | Some res -> aux nodes (res :: acc)
+        | None -> aux nodes acc)
+  in
+  aux nodes []
+
+(* util *)
+let filter_map_cut f l =
+  match List.filter_map f l with
+  | [] -> None
+  | res -> Some res
+
+(* Return list of pairs of diags, qf *)
+let get_qf (d : Lang.Diagnostic.t) : _ option =
+  Option.bind d.data (function
+    | { Lang.Diagnostic.Data.quickFix = Some qf; _ } -> Some (d, qf)
+    | _ -> None)
+
+let get_qfs ~range (doc : Fleche.Doc.t) =
+  let f { Fleche.Doc.Node.diags; _ } = filter_map_cut get_qf diags in
+  filter_map_range ~range ~nodes:doc.nodes ~f |> List.concat
+
+let request ~range ~token:_ ~(doc : Fleche.Doc.t) =
+  let kind = Some "quickfix" in
+  let isPreferred = Some true in
+  let qf = get_qfs ~range doc in
+  let bf (d, qf) =
+    List.map
+      (fun { Lang.Qf.range; newText } ->
+        let oldText =
+          Fleche.Contents.extract_raw ~contents:doc.contents ~range
+        in
+        let title = Format.asprintf "Replace `%s` by `%s`" oldText newText in
+        let diagnostics = [ d ] in
+        let qf = [ Lsp.Workspace.TextEdit.{ range; newText } ] in
+        let changes = [ (doc.uri, qf) ] in
+        let edit = Some Lsp.Workspace.WorkspaceEdit.{ changes } in
+        Lsp.Core.CodeAction.{ title; kind; diagnostics; isPreferred; edit })
+      qf
+  in
+  List.concat_map bf qf
+
+let request ~range ~token ~(doc : Fleche.Doc.t) =
+  let res = request ~range ~token ~doc in
+  Ok (`List (List.map Lsp.Core.CodeAction.to_yojson res))
diff --git a/controller/rq_action.mli b/controller/rq_action.mli
new file mode 100644
index 00000000..959b0a03
--- /dev/null
+++ b/controller/rq_action.mli
@@ -0,0 +1 @@
+val request : range:Lang.Range.t -> Request.document
diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml
index 47d672db..fa1cb142 100644
--- a/controller/rq_goals.ml
+++ b/controller/rq_goals.ml
@@ -6,7 +6,7 @@
 (************************************************************************)
 
 (* Replace by ppx when we can print goals properly in the client *)
-let mk_message (level, { Coq.Message.Payload.range; msg }) =
+let mk_message (level, { Coq.Message.Payload.range; msg; quickFix = _ }) =
   Lsp.JFleche.Message.{ range; level; text = msg }
 
 let mk_messages node =
diff --git a/controller/rq_init.ml b/controller/rq_init.ml
index 3b008cd6..b5f7bd9a 100644
--- a/controller/rq_init.ml
+++ b/controller/rq_init.ml
@@ -117,7 +117,7 @@ let do_initialize ~io ~params =
     [ ("textDocumentSync", `Int 1)
     ; ("documentSymbolProvider", `Bool true)
     ; ("hoverProvider", `Bool true)
-    ; ("codeActionProvider", `Bool false)
+    ; ("codeActionProvider", `Bool true)
     ; ( "completionProvider"
       , `Assoc
           [ ("triggerCharacters", `List [ `String "\\" ])
diff --git a/coq/init.ml b/coq/init.ml
index eaabe9ed..891075c2 100644
--- a/coq/init.ml
+++ b/coq/init.ml
@@ -36,14 +36,20 @@ let coq_lvl_to_severity (lvl : Feedback.level) =
   | Feedback.Warning -> warning
   | Feedback.Error -> error
 
-let add_message lvl range msg q =
+let qf_of_coq qf =
+  let range = Quickfix.loc qf in
+  let newText = Quickfix.pp qf |> Pp.string_of_ppcmds in
+  { Lang.Qf.range; newText }
+
+let add_message lvl range qf msg q =
   let lvl = coq_lvl_to_severity lvl in
-  let payload = Message.Payload.make ?range msg in
+  let quickFix = if qf = [] then None else Some (List.map qf_of_coq qf) in
+  let payload = Message.Payload.make ?range ?quickFix msg in
   q := (lvl, payload) :: !q
 
 let mk_fb_handler q Feedback.{ contents; _ } =
   match contents with
-  | Message (lvl, loc, _, msg) -> add_message lvl loc msg q
+  | Message (lvl, loc, qf, msg) -> add_message lvl loc qf msg q
   | _ -> ()
 
 let coq_init opts =
diff --git a/coq/message.ml b/coq/message.ml
index f48644d2..71557391 100644
--- a/coq/message.ml
+++ b/coq/message.ml
@@ -2,11 +2,15 @@
 module Payload = struct
   type 'l t =
     { range : 'l option
+    ; quickFix : 'l Lang.Qf.t list option
     ; msg : Pp.t
     }
 
-  let make ?range msg = { range; msg }
-  let map ~f { range; msg } = { range = Option.map f range; msg }
+  let make ?range ?quickFix msg = { range; quickFix; msg }
+
+  let map ~f { range; quickFix; msg } =
+    let quickFix = Option.map (List.map (Lang.Qf.map ~f)) quickFix in
+    { range = Option.map f range; quickFix; msg }
 end
 
 type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t
diff --git a/coq/message.mli b/coq/message.mli
index 2935dd5b..f6bc0957 100644
--- a/coq/message.mli
+++ b/coq/message.mli
@@ -10,10 +10,11 @@
 module Payload : sig
   type 'l t =
     { range : 'l option
+    ; quickFix : 'l Lang.Qf.t list option
     ; msg : Pp.t
     }
 
-  val make : ?range:'l -> Pp.t -> 'l t
+  val make : ?range:'l -> ?quickFix:'l Lang.Qf.t list -> Pp.t -> 'l t
   val map : f:('l -> 'm) -> 'l t -> 'm t
 end
 
diff --git a/coq/protect.ml b/coq/protect.ml
index f9560312..f6bcb736 100644
--- a/coq/protect.ml
+++ b/coq/protect.ml
@@ -27,11 +27,24 @@ module R = struct
     | Completed (Ok r) -> Completed (Ok r)
     | Interrupted -> Interrupted
 
+  (* Similar to Message.map, but missing the priority field, this is due to Coq
+     having to sources of feedback, an async one, and the exn sync one.
+     Ultimately both carry the same [payload].
+
+     See coq/coq#5479 for some information about this, among some other relevant
+     issues. AFAICT, the STM tried to use a full async error reporting however
+     due to problems the more "legacy" exn is the actuall error mechanism in
+     use *)
   let map_loc ~f =
     let f = Message.Payload.map ~f in
     map_error ~f
 end
 
+let qf_of_coq qf =
+  let range = Quickfix.loc qf in
+  let newText = Quickfix.pp qf |> Pp.string_of_ppcmds in
+  { Lang.Qf.range; newText }
+
 (* Eval and reify exceptions *)
 let eval_exn ~token ~f x =
   match Limits.limit ~token ~f x with
@@ -43,7 +56,12 @@ let eval_exn ~token ~f x =
     let e, info = Exninfo.capture exn in
     let range = Loc.(get_loc info) in
     let msg = CErrors.iprint (e, info) in
-    let payload = Message.Payload.make ?range msg in
+    let quickFix =
+      match Quickfix.from_exception exn with
+      | Ok [] | Error _ -> None
+      | Ok qf -> Some (List.map qf_of_coq qf)
+    in
+    let payload = Message.Payload.make ?range ?quickFix msg in
     Vernacstate.Interp.invalidate_cache ();
     if CErrors.is_anomaly e then R.Completed (Error (Anomaly payload))
     else R.Completed (Error (User payload))
diff --git a/coq/protect.mli b/coq/protect.mli
index cfbd6595..6868a6ad 100644
--- a/coq/protect.mli
+++ b/coq/protect.mli
@@ -28,7 +28,7 @@ module R : sig
 end
 
 module E : sig
-  type ('a, 'l) t =
+  type ('a, 'l) t = private
     { r : ('a, 'l) R.t
     ; feedback : 'l Message.t list
     }
diff --git a/examples/Pff.v b/examples/Pff.v
index 252b89f3..3db572bd 100644
--- a/examples/Pff.v
+++ b/examples/Pff.v
@@ -14,7 +14,7 @@ Require Import Psatz.
 Set Warnings "-deprecated".
 
 (* Compatibility workaround, remove once requiring Coq >= 8.16 *)
-Module Import Compat.
+Module Import Compat816.
 
 Lemma Even_0 : Nat.Even 0.
 Proof. exists 0; reflexivity. Qed.
@@ -67,7 +67,21 @@ Proof proj1 (proj1 (Even_Odd_double n)).
 Definition Odd_double n : Nat.Odd n -> n = S (Nat.double (Nat.div2 n)).
 Proof proj1 (proj2 (Even_Odd_double n)).
 
-End Compat.
+Definition Rinv_mult_distr := Rinv_mult_distr.
+Definition Rabs_Rinv := Rabs_Rinv.
+Definition Rinv_pow := Rinv_pow.
+Definition Rinv_involutive := Rinv_involutive.
+Definition Rlt_Rminus := Rlt_Rminus.
+Definition powerRZ_inv := powerRZ_inv.
+Definition powerRZ_neg := powerRZ_neg.
+
+End Compat816.
+
+Module Import Compat819.
+
+Definition IZR_neq := IZR_neq.
+
+End Compat819.
 
 (*** was file sTactic.v  ***)
 
@@ -17553,7 +17567,7 @@ apply Z.le_trans with  (Nat.double (Nat.div2 t)).
 unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Even_double; auto with zarith.
 apply Z.le_trans with (-1+(S ( Nat.double (Nat.div2 t))))%Z.
-rewrite inj_S; unfold Z.succ; auto with zarith.
+rewrite inj_S; unfold Z.succ; auto with zarith;
 unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Odd_double by easy. lia.
 Qed.
@@ -17568,9 +17582,9 @@ case (Nat.Even_or_Odd t); intros I.
 apply Z.le_trans with  ((Nat.double (Nat.div2 t)+1))%Z.
 2:unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Even_double; auto with zarith.
-apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith.
-2: rewrite inj_S; unfold Z.succ; auto with zarith.
-2: unfold Nat.double; rewrite inj_plus; auto with zarith.
+apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith;
+try solve [rewrite inj_S; unfold Z.succ; auto with zarith;
+  unfold Nat.double; rewrite inj_plus; auto with zarith].
 rewrite <- Odd_double; auto with zarith.
 Qed.
 
diff --git a/examples/codeAction.v b/examples/codeAction.v
new file mode 100644
index 00000000..e56fd402
--- /dev/null
+++ b/examples/codeAction.v
@@ -0,0 +1,54 @@
+(* Test for Coq's QF for Coq to Stdlib PRs *)
+
+Require Import Coq.ssr.ssrbool.
+From Coq Require Import ssreflect ssrbool.
+
+(* Note: this tests the two different lookup modes *)
+About Coq.Init.Nat.add.
+Check Coq.Init.Nat.add.
+
+(* Example codeAction, from Coq's test suite *)
+
+Module M. Definition y := 4. End M.
+Import M.
+
+#[deprecated(use=y)]
+Definition x := 3.
+
+Module N. Definition y := 5. End N.
+Import N.
+
+Definition d1 := x = 3.
+
+Module M1.
+Notation w := x.
+End M1.
+Import M1.
+
+#[deprecated(use=w)]
+Notation v := 3.
+
+Module M2.
+Notation w := 5.
+End M2.
+Import M2.
+
+Definition d2 := v = 3.
+
+Fail #[deprecated(use=w)]
+Notation "a +++ b" := (a + b) (at level 2).
+
+Fail #[deprecated(use=nonexisting)]
+Definition y := 2.
+
+(***********************************************)
+Module A.
+End B.
+
+(***********************************************)
+Require Import Extraction.
+
+Module nat. End nat.
+
+Extraction nat.
+
diff --git a/fleche/doc.ml b/fleche/doc.ml
index cd73263e..bb06a0cc 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -155,6 +155,7 @@ module Diags : sig
   (** Build advanced diagnostic with AST analysis *)
   val error :
        err_range:Lang.Range.t
+    -> quickFix:Lang.Range.t Lang.Qf.t list option
     -> msg:Pp.t
     -> stm_range:Lang.Range.t (* range for the sentence *)
     -> ?ast:Node.Ast.t
@@ -175,7 +176,7 @@ end = struct
     Lang.Diagnostic.{ range; severity; message; data }
 
   (* ast-dependent error diagnostic generation *)
-  let extra_diagnostics_of_ast stm_range ast =
+  let extra_diagnostics_of_ast quickFix stm_range ast =
     let sentenceRange = Some stm_range in
     let failedRequire =
       match
@@ -187,21 +188,29 @@ end = struct
         Some [ { Lang.Diagnostic.FailedRequire.prefix = from; refs } ]
       | _ -> None
     in
-    Some { Lang.Diagnostic.Data.sentenceRange; failedRequire }
+    Some { Lang.Diagnostic.Data.sentenceRange; failedRequire; quickFix }
 
-  let extra_diagnostics_of_ast stm_range ast =
+  let extra_diagnostics_of_ast qf stm_range ast =
     if !Config.v.send_diags_extra_data then
-      extra_diagnostics_of_ast stm_range ast
+      extra_diagnostics_of_ast qf stm_range ast
     else None
 
-  let error ~err_range ~msg ~stm_range ?ast () =
-    let data = extra_diagnostics_of_ast stm_range ast in
+  let error ~err_range ~quickFix ~msg ~stm_range ?ast () =
+    let data = extra_diagnostics_of_ast quickFix stm_range ast in
     make ?data err_range Lang.Diagnostic.Severity.error msg
 
   let of_feed ~drange (severity, payload) =
-    let { Coq.Message.Payload.range; msg } = payload in
+    let { Coq.Message.Payload.range; quickFix; msg } = payload in
     let range = Option.default drange range in
-    make range severity msg
+    (* Be careful to avoid defining data if quickFix = None *)
+    let data =
+      Option.map
+        (fun qf ->
+          let sentenceRange, failedRequire, quickFix = (None, None, Some qf) in
+          Lang.Diagnostic.Data.{ sentenceRange; failedRequire; quickFix })
+        quickFix
+    in
+    make ?data range severity msg
 
   type partition_kind =
     | Left
@@ -400,8 +409,8 @@ let handle_doc_creation_exec ~token ~env ~uri ~version ~contents =
       let message = "Document Creation Interrupted!" in
       let range = None in
       error_doc ~range ~message ~uri ~version ~contents ~env
-    | Completed (Error (User { range; msg = err_msg }))
-    | Completed (Error (Anomaly { range; msg = err_msg })) ->
+    | Completed (Error (User { range; msg = err_msg; quickFix = _ }))
+    | Completed (Error (Anomaly { range; msg = err_msg; quickFix = _ })) ->
       let message =
         Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with err_msg
       in
@@ -663,6 +672,7 @@ end = struct
     | Completed (Ok st) -> st
     | Completed (Error _) -> st
 end
+(* end [module Recovery = struct...] *)
 
 let interp_and_info ~token ~st ~files ast =
   match Coq.Ast.Require.extract ast with
@@ -753,22 +763,23 @@ let parse_action ~token ~lines ~st last_tok doc_handle =
     | Ok (Some ast) ->
       let () = if Debug.parsing then DDebug.parsed_sentence ~ast in
       (Process ast, [], feedback, time)
-    | Error (Anomaly { msg; _ }) | Error (User { range = None; msg }) ->
+    | Error (Anomaly { range = _; quickFix; msg })
+    | Error (User { range = None; quickFix; msg }) ->
       (* We don't have a better alternative :(, usually missing error loc here
          means an anomaly, so we stop *)
       let err_range = last_tok in
       let parse_diags =
-        [ Diags.error ~err_range ~msg ~stm_range:err_range () ]
+        [ Diags.error ~err_range ~quickFix ~msg ~stm_range:err_range () ]
       in
       (EOF (Failed last_tok), parse_diags, feedback, time)
-    | Error (User { range = Some err_range; msg }) ->
+    | Error (User { range = Some err_range; quickFix; msg }) ->
       Coq.Parsing.discard_to_dot doc_handle;
       let last_tok = Coq.Parsing.Parsable.loc doc_handle in
       let last_tok_range = Coq.Utils.to_range ~lines last_tok in
       let span_loc = Util.build_span start_loc last_tok in
       let span_range = Coq.Utils.to_range ~lines span_loc in
       let parse_diags =
-        [ Diags.error ~err_range ~msg ~stm_range:span_range () ]
+        [ Diags.error ~err_range ~quickFix ~msg ~stm_range:span_range () ]
       in
       (Skip (span_range, last_tok_range), parse_diags, feedback, time))
 
@@ -820,10 +831,13 @@ let node_of_coq_result ~token ~doc ~range ~prev ~ast ~st ~parsing_diags
         ~diags:[] ~feedback ~info
     in
     Continue { state; last_tok; node }
-  | Error (Coq.Protect.Error.Anomaly { range = err_range; msg } as coq_err)
-  | Error (User { range = err_range; msg } as coq_err) ->
+  | Error
+      (Coq.Protect.Error.Anomaly { range = err_range; quickFix; msg } as coq_err)
+  | Error (User { range = err_range; quickFix; msg } as coq_err) ->
     let err_range = Option.default range err_range in
-    let err_diags = [ Diags.error ~err_range ~msg ~stm_range:range ~ast () ] in
+    let err_diags =
+      [ Diags.error ~err_range ~quickFix ~msg ~stm_range:range ~ast () ]
+    in
     let contents, nodes = (doc.contents, doc.nodes) in
     let context =
       Recovery_context.make ~contents ~last_tok ~nodes ~ast:ast.v ()
diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml
index db01508c..f88f4902 100644
--- a/lang/diagnostic.ml
+++ b/lang/diagnostic.ml
@@ -15,6 +15,7 @@ module Data = struct
   type t =
     { sentenceRange : Range.t option [@default None]
     ; failedRequire : FailedRequire.t list option [@default None]
+    ; quickFix : Range.t Qf.t list option [@default None]
     }
 end
 
diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli
index 1087171f..7368ab86 100644
--- a/lang/diagnostic.mli
+++ b/lang/diagnostic.mli
@@ -15,6 +15,7 @@ module Data : sig
   type t =
     { sentenceRange : Range.t option [@default None]
     ; failedRequire : FailedRequire.t list option [@default None]
+    ; quickFix : Range.t Qf.t list option [@default None]
     }
 end
 
diff --git a/lang/qf.ml b/lang/qf.ml
new file mode 100644
index 00000000..15d64593
--- /dev/null
+++ b/lang/qf.ml
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* Flèche => document manager: Language Support                         *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+type 'l t =
+  { range : 'l
+  ; newText : string
+  }
+
+let map ~f { range; newText } = { range = f range; newText }
diff --git a/lang/qf.mli b/lang/qf.mli
new file mode 100644
index 00000000..c3965d04
--- /dev/null
+++ b/lang/qf.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* Flèche => document manager: Language Support                         *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+type 'l t =
+  { range : 'l
+  ; newText : string
+  }
+
+val map : f:('l -> 'm) -> 'l t -> 'm t
diff --git a/lsp/core.ml b/lsp/core.ml
index 7284656c..24799f4c 100644
--- a/lsp/core.ml
+++ b/lsp/core.ml
@@ -177,3 +177,33 @@ module DocumentDiagnosticReportPartialResult = struct
     }
   [@@deriving to_yojson]
 end
+
+(* CodeAction *)
+module CodeActionContext = struct
+  type t =
+    { diagnostics : Lang.Diagnostic.t list
+    ; only : string option [@default None]
+    ; triggerKind : int option [@default None]
+    }
+  [@@deriving to_yojson]
+end
+
+module CodeActionParams = struct
+  type t =
+    { textDocument : Doc.TextDocumentIdentifier.t
+    ; range : Lang.Range.t
+    ; context : CodeActionContext.t
+    }
+  [@@deriving to_yojson]
+end
+
+module CodeAction = struct
+  type t =
+    { title : string
+    ; kind : string option [@default None]
+    ; diagnostics : Lang.Diagnostic.t list [@default []]
+    ; isPreferred : bool option [@default None]
+    ; edit : Workspace.WorkspaceEdit.t option [@default None]
+    }
+  [@@deriving to_yojson]
+end
diff --git a/lsp/core.mli b/lsp/core.mli
index ae706ef8..c222d34e 100644
--- a/lsp/core.mli
+++ b/lsp/core.mli
@@ -180,3 +180,33 @@ module DocumentDiagnosticReportPartialResult : sig
     }
   [@@deriving to_yojson]
 end
+
+(* CodeAction *)
+module CodeActionContext : sig
+  type t =
+    { diagnostics : Lang.Diagnostic.t list
+    ; only : string option [@default None]
+    ; triggerKind : int option [@default None]
+    }
+  [@@deriving to_yojson]
+end
+
+module CodeActionParams : sig
+  type t =
+    { textDocument : Doc.TextDocumentIdentifier.t
+    ; range : Lang.Range.t
+    ; context : CodeActionContext.t
+    }
+  [@@deriving to_yojson]
+end
+
+module CodeAction : sig
+  type t =
+    { title : string
+    ; kind : string option [@default None]
+    ; diagnostics : Lang.Diagnostic.t list [@default []]
+    ; isPreferred : bool option [@default None]
+    ; edit : Workspace.WorkspaceEdit.t option [@default None]
+    }
+  [@@deriving to_yojson]
+end
diff --git a/lsp/jCoq.ml b/lsp/jCoq.ml
index 3497091a..fabdda66 100644
--- a/lsp/jCoq.ml
+++ b/lsp/jCoq.ml
@@ -26,6 +26,7 @@ let rec pp_opt d =
 module Pp = struct
   include Serlib.Ser_pp
 
+  let str = Pp.str
   let string_of_ppcmds = Pp.string_of_ppcmds
   let to_string = Pp.string_of_ppcmds
   let to_yojson x = to_yojson (pp_opt x)
diff --git a/lsp/jLang.ml b/lsp/jLang.ml
index 631d902a..a486ac03 100644
--- a/lsp/jLang.ml
+++ b/lsp/jLang.ml
@@ -34,6 +34,10 @@ module LUri = struct
   end
 end
 
+module Qf = struct
+  type 'l t = [%import: 'l Lang.Qf.t] [@@deriving yojson]
+end
+
 module Diagnostic = struct
   module Libnames = Serlib.Ser_libnames
 
@@ -44,6 +48,7 @@ module Diagnostic = struct
   module Data = struct
     module Lang = struct
       module Range = Range
+      module Qf = Qf
       module FailedRequire = FailedRequire
       module Diagnostic = Lang.Diagnostic
     end
@@ -61,6 +66,7 @@ module Diagnostic = struct
     [@@deriving yojson]
 
     let conv { Lang.Point.line; character; offset = _ } = { line; character }
+    let vnoc { line; character } = { Lang.Point.line; character; offset = -1 }
   end
 
   module Range = struct
@@ -74,6 +80,11 @@ module Diagnostic = struct
       let start = Point.conv start in
       let end_ = Point.conv end_ in
       { start; end_ }
+
+    let vnoc { start; end_ } =
+      let start = Point.vnoc start in
+      let end_ = Point.vnoc end_ in
+      { Lang.Range.start; end_ }
   end
 
   (* Current Flèche diagnostic is not LSP-standard compliant, this one is *)
@@ -91,6 +102,14 @@ module Diagnostic = struct
     let range = Range.conv range in
     let message = Pp.to_string message in
     _t_to_yojson { range; severity; message; data }
+
+  let of_yojson json =
+    match _t_of_yojson json with
+    | Ok { range; severity; message; data } ->
+      let range = Range.vnoc range in
+      let message = Pp.str message in
+      Ok { Lang.Diagnostic.range; severity; message; data }
+    | Error err -> Error err
 end
 
 module Stdlib = JStdlib
diff --git a/lsp/jLang.mli b/lsp/jLang.mli
index 2b59f7b8..11b624c0 100644
--- a/lsp/jLang.mli
+++ b/lsp/jLang.mli
@@ -20,7 +20,7 @@ module LUri : sig
 end
 
 module Diagnostic : sig
-  type t = Lang.Diagnostic.t [@@deriving to_yojson]
+  type t = Lang.Diagnostic.t [@@deriving yojson]
 
   module Point : sig
     type t =
@@ -36,6 +36,8 @@ module Diagnostic : sig
       ; end_ : Point.t [@key "end"]
       }
     [@@deriving yojson]
+
+    val vnoc : t -> Lang.Range.t
   end
 end
 
diff --git a/lsp/workspace.ml b/lsp/workspace.ml
index d457453f..912037ee 100644
--- a/lsp/workspace.ml
+++ b/lsp/workspace.ml
@@ -4,6 +4,7 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+module Lang_ = Lang
 module Lang = JLang
 
 module WorkspaceFolder = struct
@@ -25,3 +26,23 @@ end
 module DidChangeWorkspaceFoldersParams = struct
   type t = { event : WorkspaceFoldersChangeEvent.t } [@@deriving yojson]
 end
+
+module TextEdit = struct
+  type t =
+    { range : Lang.Range.t
+    ; newText : string
+    }
+  [@@deriving yojson]
+end
+
+module WorkspaceEdit = struct
+  type t = { changes : (Lang.LUri.File.t * TextEdit.t list) list }
+  [@@deriving of_yojson]
+
+  let tok (uri, edits) =
+    ( Lang_.LUri.File.to_string_uri uri
+    , `List (List.map TextEdit.to_yojson edits) )
+
+  let to_yojson { changes } =
+    `Assoc [ ("changes", `Assoc (List.map tok changes)) ]
+end
diff --git a/lsp/workspace.mli b/lsp/workspace.mli
index f8b85633..ae684d56 100644
--- a/lsp/workspace.mli
+++ b/lsp/workspace.mli
@@ -23,3 +23,16 @@ end
 module DidChangeWorkspaceFoldersParams : sig
   type t = { event : WorkspaceFoldersChangeEvent.t } [@@deriving yojson]
 end
+
+module TextEdit : sig
+  type t =
+    { range : Lang.Range.t
+    ; newText : string
+    }
+  [@@deriving yojson]
+end
+
+module WorkspaceEdit : sig
+  type t = { changes : (Lang.LUri.File.t * TextEdit.t list) list }
+  [@@deriving yojson]
+end
diff --git a/vendor/coq b/vendor/coq
index b6805232..6633e815 160000
--- a/vendor/coq
+++ b/vendor/coq
@@ -1 +1 @@
-Subproject commit b68052328b65a3e85cd48a4718713fdd0c24f08d
+Subproject commit 6633e8151afa194ea8378ac3598564cfbf571ca4