diff --git a/client/src/extension.ts b/client/src/extension.ts
index 33d93ac42..38b456f4c 100644
--- a/client/src/extension.ts
+++ b/client/src/extension.ts
@@ -9,7 +9,8 @@ import {workspace, window, commands, languages, ExtensionContext, env,
   extensions,
   StatusBarAlignment,
   MarkdownString,
-  WorkspaceEdit
+  WorkspaceEdit,
+  Position
 } from 'vscode';
 
 import {
@@ -27,6 +28,8 @@ import GoalPanel from './panels/GoalPanel';
 import SearchViewProvider from './panels/SearchViewProvider';
 import {
     CoqLogMessage,
+    CoqPilotRequest,
+    CoqPilotResponse,
     DocumentProofsRequest,
     DocumentProofsResponse,
     ErrorAlertNotification,
@@ -61,6 +64,14 @@ export function activate(context: ExtensionContext) {
         return client.sendRequest(req, params);
     };
 
+    const runTacticsAtLocContext = (uri: Uri, position: Position, text: string) => {
+        const textDocument = TextDocumentIdentifier.create(uri.toString());
+        const params: CoqPilotRequest = {textDocument, position, text};
+        const req = new RequestType<CoqPilotRequest, CoqPilotResponse, void>("vscoq/coqPilot");
+        Client.writeToVscoq2Channel("Trying running tactics: (" + text + ") for document: " + uri.toString());
+        return client.sendRequest(req, params);
+    };
+    
     const coqTM = new VsCoqToolchainManager();
     coqTM.intialize().then(
         () => {
@@ -370,7 +381,8 @@ Path: \`${coqTM.getVsCoqTopPath()}\`
     }
 
     const externalApi = {
-        getDocumentProofs
+        getDocumentProofs,
+        runTacticsAtLocContext
     };
 
     return externalApi;
diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts
index c72a3e8a3..377439993 100644
--- a/client/src/protocol/types.ts
+++ b/client/src/protocol/types.ts
@@ -168,3 +168,13 @@ type ProofBlock = {
 export interface DocumentProofsResponse {
     proofs: ProofBlock[];
 }
+
+export interface CoqPilotRequest {
+    textDocument: TextDocumentIdentifier;
+    position: Position;
+    text: string;
+}
+
+export interface CoqPilotResponse {
+    errors: string[];
+}
diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
index a94498d9c..b6db7cfae 100644
--- a/language-server/dm/document.ml
+++ b/language-server/dm/document.ml
@@ -112,7 +112,7 @@ type parse_state = {
   loc: Loc.t option;
   synterp_state : Vernacstate.Synterp.t;
   stream: (unit, char) Gramlib.Stream.t;
-  raw: RawDocument.t;
+  raw: RawDocument.t option;
   parsed: pre_sentence list;
   errors: parsing_error list;
   parsed_comments: comment list;
@@ -269,6 +269,20 @@ let add_sentence parsed parsing_start start stop (ast: sentence_state) synterp_s
   } in
   document, scheduler_state_after
 
+let pre_sentence_to_sentence parsing_start start stop (ast: sentence_state) synterp_state scheduler_state_before schedule =
+  let id = Stateid.fresh () in
+  let scheduler_state_after, schedule = 
+    match ast with
+    | Error {msg} ->
+      scheduler_state_before, Scheduler.schedule_errored_sentence id msg schedule
+    | Parsed ast ->
+      let ast' = (ast.ast, ast.classification, synterp_state) in
+      Scheduler.schedule_sentence (id, ast') scheduler_state_before schedule
+  in
+  (* FIXME may invalidate scheduler_state_XXX for following sentences -> propagate? *)
+  let sentence = { parsing_start; start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in
+  sentence, schedule, scheduler_state_after
+  
 let remove_sentence parsed id =
   match SM.find_opt id parsed.sentences_by_id with
   | None -> parsed
@@ -561,7 +575,7 @@ let handle_parse_error start parsing_start msg qf ({stream; errors; parsed;} as
   let errors = parsing_error :: errors in
   let parse_state = {parse_state with errors; parsed} in
   (* TODO: we could count the \n between start and stop and increase Loc.line_nb *)
-  create_parsing_event (ParseEvent parse_state)
+  ParseEvent parse_state
 
 let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments} as parse_state) =
   let start = Stream.count stream in
@@ -569,7 +583,7 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
   begin
     (* FIXME should we save lexer state? *)
     match parse_one_sentence ?loc stream ~st:synterp_state with
-    | None, _ (* EOI *) -> create_parsing_event (Invalidate parse_state)
+    | None, _ (* EOI *) -> Invalidate parse_state
     | Some ast, comments ->
       let stop = Stream.count stream in
       let begin_line, begin_char, end_char =
@@ -577,10 +591,14 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
               | Some lc -> lc.line_nb, lc.bp, lc.ep
               | None -> assert false
       in
-      let str = String.sub (RawDocument.text raw) begin_char (end_char - begin_char) in
-      let sstr = Stream.of_string str in
-      let lex = CLexer.Lexer.tok_func sstr in
-      let tokens = stream_tok 0 [] lex begin_line begin_char in
+        let tokens = match raw with
+        | None -> []
+        | Some raw ->
+          let str = String.sub (RawDocument.text raw) begin_char (end_char - begin_char) in
+          let sstr = Stream.of_string str in
+          let lex = CLexer.Lexer.tok_func sstr in
+          stream_tok 0 [] lex begin_line begin_char
+        in
       begin
         try
           log (fun () -> "Parsed: " ^ (Pp.string_of_ppcmds @@ Ppvernac.pr_vernac ast));
@@ -594,7 +612,7 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
           let parsed_comments = List.append comments parsed_comments in
           let loc = ast.loc in
           let parse_state = {parse_state with parsed_comments; parsed; loc; synterp_state} in
-          create_parsing_event (ParseEvent parse_state)
+          ParseEvent parse_state
         with exn ->
           let e, info = Exninfo.capture exn in
           let loc = get_loc_from_info_or_exn e info in
@@ -678,7 +696,7 @@ let validate_document ({ parsed_loc; raw_doc; cancel_handle } as document) =
   while Stream.count stream < stop do Stream.junk () stream done;
   log (fun () -> Format.sprintf "Parsing more from pos %i" stop);
   let started = Unix.gettimeofday () in
-  let parsed_state = {stop; top_id;synterp_state; stream; raw=raw_doc; parsed=[]; errors=[]; parsed_comments=[]; loc=None; started; previous_document=document} in
+  let parsed_state = {stop; top_id;synterp_state; stream; raw=(Some raw_doc); parsed=[]; errors=[]; parsed_comments=[]; loc=None; started; previous_document=document} in
   let priority = Some PriorityManager.parsing in
   let event = Sel.now ?priority (ParseEvent parsed_state) in
   let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in
@@ -711,10 +729,31 @@ let handle_invalidate {parsed; errors; parsed_comments; stop; top_id; started; p
 let handle_event document = function
 | ParseEvent state -> 
   let event = handle_parse_more state in
+  let event = create_parsing_event event in
   let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in
   {document with cancel_handle}, [event], None
 | Invalidate state -> {document with cancel_handle=None}, [], handle_invalidate state document
 
+let rec parse_full = function
+| ParseEvent state ->
+  let event = handle_parse_more state in
+  parse_full event
+| Invalidate state ->
+  state
+
+let parse_text_at_loc loc text document =
+  let top_id = Option.map (fun sentence -> sentence.id) (find_sentence_strictly_before document loc) in
+  let (stop, synterp_state, scheduler_state) = state_strictly_before document loc in
+  let stream = Stream.of_string text in
+  let parsed_state = {synterp_state; started = Unix.gettimeofday (); top_id; stream; raw=None; loc=None; errors=[]; parsed=[]; parsed_comments=[]; previous_document=document; stop} in
+  let {parsed} = parse_full (ParseEvent parsed_state) in
+  let add_sentence (sentences, schedule, scheduler_state) ({ parsing_start; start; stop; ast; synterp_state } : pre_sentence) =
+    let added_sentence, schedule, schedule_state = pre_sentence_to_sentence parsing_start start stop ast synterp_state scheduler_state schedule in
+    sentences @ [added_sentence], schedule, schedule_state
+  in
+  let sentences, schedule, _ = List.fold_left add_sentence ([],document.schedule, scheduler_state) parsed in
+  sentences, schedule
+
 let create_document init_synterp_state text =
   let raw_doc = RawDocument.create text in
     { 
diff --git a/language-server/dm/document.mli b/language-server/dm/document.mli
index 60ddc2eae..b0a0b57fe 100644
--- a/language-server/dm/document.mli
+++ b/language-server/dm/document.mli
@@ -166,6 +166,8 @@ val range_of_id : document -> Stateid.t -> Range.t
 val range_of_id_with_blank_space : document -> Stateid.t -> Range.t
 (** [range_of_id_with_blank_space doc id] returns a Range object coressponding to the sentence id given in argument but with the white spaces before (until the previous sentence) *)
 
+val parse_text_at_loc : int -> string -> document -> sentence list * Scheduler.schedule
+
 module Internal : sig
 
   val string_of_sentence : sentence -> string
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 06bc305f6..da78bbf38 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -331,6 +331,30 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve
 
 let reset_to_top st = { st with observe_id = Top }
 
+let coq_pilot_observe st position text =
+  let loc = RawDocument.loc_of_position (Document.raw_document st.document) position in
+  match Document.find_sentence_before st.document loc with
+  | None -> log @@ (fun () -> "COQ PILOT ON NON VALID POSITION"); [] (* HANDLE ERROR *)
+  | Some {id} ->
+    let sentences, sch = Document.parse_text_at_loc loc text st.document in
+    let vst_for_next_todo, execution_state, _, _ = ExecutionManager.build_tasks_for st.document (Document.schedule st.document) st.execution_state id false in
+    let task, execution_state_after = ExecutionManager.build_tasks_for_sentences execution_state sch sentences in
+    let rec execute_task execution_state vst_for_next_todo task =
+      match task with
+      | None -> log(fun() -> "NO TASK TO EXECUTE"); execution_state, vst_for_next_todo
+      | Some task ->
+        log(fun () -> "EXECUTING TASK");
+        let (next, execution_state,vst_for_next_todo,_events,_interrupted) =
+        ExecutionManager.execute_with_no_overview execution_state (vst_for_next_todo, [], false) task false in
+        execute_task execution_state vst_for_next_todo next
+    in
+    let execution_state_after, _ = execute_task execution_state_after vst_for_next_todo task in
+    let all_errors_before = ExecutionManager.all_errors execution_state in
+    let all_errors = ExecutionManager.all_errors execution_state_after in
+    let is_not_in_error_list (id, _) errors = List.find_opt (fun (e_id, _) -> e_id = id) errors = None in
+    let all_errors = List.filter (fun e -> is_not_in_error_list e all_errors_before)  all_errors in
+    let get_pp_error (_, (_, pp, _)) = pp in
+    List.map (fun e -> Pp.string_of_ppcmds @@  get_pp_error e) all_errors
 
 let get_document_proofs st =
   let outline = Document.outline st.document in
diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
index d7cc35716..bf38ae5cc 100644
--- a/language-server/dm/documentManager.mli
+++ b/language-server/dm/documentManager.mli
@@ -142,6 +142,7 @@ val locate : state -> Position.t -> pattern:string -> (pp, error) Result.t
 
 val print : state -> Position.t -> pattern:string -> (pp, error) Result.t
 
+val coq_pilot_observe : state -> Position.t -> string -> string list
 
 module Internal : sig
 
diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 51ca8b185..875b54db8 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -682,6 +682,19 @@ let execute st document (vs, events, interrupted) task block_on_first_error =
     let st = { st with todo=[]} in
     None, st, vst_for_next_todo, events, exec_error
 
+let execute_with_no_overview st (vs, events, interrupted) task block_on_first_error =
+  let st, vst_for_next_todo, events, _, exec_error =
+    execute_task st (vs, events, interrupted) task in
+  match block_on_first_error, exec_error with
+  | false, _ | _, None ->
+    let next, st = match st.todo with
+      | [] -> None, st
+      | task :: todo -> Some task, { st with todo }
+    in next, st, vst_for_next_todo, events, None
+  | true, Some _ ->
+    let st = { st with todo=[]} in
+    None, st, vst_for_next_todo, events, exec_error
+
 
 let build_tasks_for document sch st id block =
   let rec build_tasks id tasks st =
@@ -727,6 +740,14 @@ let build_tasks_for document sch st id block =
   | Some id, true ->
     vs, {st with todo=[]}, None, Some id
 
+let build_tasks_for_sentences st sch sentences =
+  let tasks = List.map (fun ({id}: Document.sentence) -> snd @@ task_for_sentence sch id) sentences in
+  let todo = List.concat_map prepare_task tasks in
+  match todo with
+  | task :: todo ->
+    Some task, {st with todo}
+  | [] -> None, st
+
 let all_errors st =
   List.fold_left (fun acc (id, (p,_)) ->
     match p with
diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli
index 0dca44162..46a758ea1 100644
--- a/language-server/dm/executionManager.mli
+++ b/language-server/dm/executionManager.mli
@@ -75,7 +75,9 @@ val handle_event : event -> state -> (sentence_id option * state option * events
 type prepared_task
 val get_id_of_executed_task : prepared_task -> sentence_id
 val build_tasks_for : Document.document -> Scheduler.schedule -> state -> sentence_id -> bool -> Vernacstate.t * state * prepared_task option * errored_sentence
+val build_tasks_for_sentences : state -> Scheduler.schedule -> Document.sentence list -> prepared_task option * state
 val execute : state -> Document.document -> Vernacstate.t * events * bool -> prepared_task -> bool -> (prepared_task option * state * Vernacstate.t * events * errored_sentence)
+val execute_with_no_overview : state -> Vernacstate.t * events * bool -> prepared_task -> bool -> (prepared_task option * state * Vernacstate.t * events * errored_sentence)
 
 (* val update_overview : prepared_task -> prepared_task list -> state -> Document.document -> state
 val cut_overview : prepared_task -> state -> Document.document -> state *)
diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
index ca863b134..69a2fabde 100644
--- a/language-server/protocol/extProtocol.ml
+++ b/language-server/protocol/extProtocol.ml
@@ -253,6 +253,15 @@ module Request = struct
     type t = {
       textDocument: TextDocumentIdentifier.t
     } [@@deriving yojson]
+    
+  end
+  module CoqPilotParams = struct
+
+    type t = {
+      textDocument : TextDocumentIdentifier.t;
+      position: Position.t;
+      text: string;
+    } [@@deriving yojson]
 
   end
 
@@ -260,6 +269,13 @@ module Request = struct
     
     type t = {
       proofs: ProofState.proof_block list;
+    } [@@ deriving yojson]
+  
+  end
+  module CoqPilotResult = struct
+
+    type t = {
+      errors: string list;
     } [@@deriving yojson]
 
   end
@@ -274,6 +290,7 @@ module Request = struct
   | Search : SearchParams.t -> unit t
   | DocumentState : DocumentStateParams.t -> DocumentStateResult.t t
   | DocumentProofs : DocumentProofsParams.t -> DocumentProofsResult.t t
+  | CoqPilot : CoqPilotParams.t -> CoqPilotResult.t t
 
   type packed = Pack : 'a t -> packed
 
@@ -304,6 +321,9 @@ module Request = struct
     | "vscoq/documentProofs" ->
       let+ params = Lsp.Import.Json.message_params params DocumentProofsParams.t_of_yojson in
       Pack (DocumentProofs params)
+    | "vscoq/coqPilot" ->
+      let+ params = Lsp.Import.Json.message_params params CoqPilotParams.t_of_yojson in
+      Pack (CoqPilot params)
     | _ ->
       let+ E req = Lsp.Client_request.of_jsonrpc req in
       Pack (Std req)
@@ -319,6 +339,7 @@ module Request = struct
       | Search _ -> yojson_of_unit resp
       | DocumentState _ -> DocumentStateResult.(yojson_of_t resp)
       | DocumentProofs _ -> DocumentProofsResult.(yojson_of_t resp)
+      | CoqPilot _ -> CoqPilotResult.(yojson_of_t resp)
       | Std req -> Lsp.Client_request.yojson_of_result req resp
 
   end
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index ff84ecf0b..c7e89da1b 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -527,6 +527,17 @@ let sendDocumentProofs id params =
       let proofs = Dm.DocumentManager.get_document_proofs st in
       Ok Request.Client.DocumentProofsResult.{ proofs }, []
 
+let sendCoqPilotResult id params =
+  let Request.Client.CoqPilotParams.{ textDocument; position; text} = params in
+  let uri = textDocument.uri in
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ (fun () -> "[coqPilotResult] ignoring event on non existant document"); Error({message="Document does not exist"; code=None}), []
+  | Some { st } -> 
+    let errors = Dm.DocumentManager.coq_pilot_observe st position text in
+    log (fun () -> "Sending errors for coqpilot request:");
+    List.iter (fun e -> log (fun () -> e)) errors;
+    Ok Request.Client.CoqPilotResult.{ errors }, []
+
 let workspaceDidChangeConfiguration params = 
   let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in
   let settings = Settings.t_of_yojson settings in
@@ -564,6 +575,7 @@ let dispatch_request : type a. Jsonrpc.Id.t -> a Request.Client.t -> (a,error) r
   | Search params -> coqtopSearch id params
   | DocumentState params -> sendDocumentState id params
   | DocumentProofs params -> sendDocumentProofs id params
+  | CoqPilot params -> log (fun() -> "Recieved request: vscoq/coqPilot"); sendCoqPilotResult id params
 
 let dispatch_std_notification = 
   let open Lsp.Client_notification in function