From 35e54a2007231bb2da8207ebaf44bd5cf82cb613 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= <maxime.denes@inria.fr>
Date: Mon, 21 Aug 2023 16:16:14 +0200
Subject: [PATCH 01/31] Test against Coq's master

---
 .github/workflows/ci.yml                   | 10 ++++++++++
 flake.nix                                  |  2 +-
 language-server/build-windows-platform.bat |  6 +++---
 language-server/vscoq-language-server.opam |  4 ++--
 4 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a451d042a..9e0396043 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -6,6 +6,9 @@ on:
   pull_request:
   workflow_dispatch:
 
+env:
+  PIN_COQ: fbaea89860348ca2b2ca485e52df7215bea27746 # Should be kept in sync with input in flake.nix
+
 jobs:
   build-extension:
     strategy:
@@ -131,6 +134,13 @@ jobs:
       with:
         ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
+    - name: Pin Coq
+      env:
+        OPAMYES: true
+      run: |
+        opam pin add coq-core.dev "https://github.com/coq/coq.git#$PIN_COQ"
+        opam pin add coq-stdlib.dev "https://github.com/coq/coq.git#$PIN_COQ"
+
     - name: Install deps
       env:
         OPAMYES: true
diff --git a/flake.nix b/flake.nix
index f9d4e78a6..3c97eceb5 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,7 +5,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    coq-master = { url = "github:coq/coq/master"; };
+    coq-master = { url = "github:coq/coq/master/fbaea89860348ca2b2ca485e52df7215bea27746"; }; # Should be kept in sync with PIN_COQ in CI workflow
     coq-master.inputs.nixpkgs.follows = "nixpkgs";
 
   };
diff --git a/language-server/build-windows-platform.bat b/language-server/build-windows-platform.bat
index 01d531fa7..3716033a5 100644
--- a/language-server/build-windows-platform.bat
+++ b/language-server/build-windows-platform.bat
@@ -31,9 +31,9 @@ call coq_platform_make_windows.bat ^
   -jobs=2 ^
   -switch=d ^
   -set-switch=y ^
-  -override-dev-pkg="coq-core=https://github.com/coq/coq/archive/%COQ_VERSION%.tar.gz" ^
-  -override-dev-pkg="coq-stdlib=https://github.com/coq/coq/archive/%COQ_VERSION%.tar.gz" ^
-  -override-dev-pkg="coq=https://github.com/coq/coq/archive/%COQ_VERSION%.tar.gz" ^
+  -override-dev-pkg="coq-core=https://github.com/coq/coq/archive/%PIN_COQ%.tar.gz" ^
+  -override-dev-pkg="coq-stdlib=https://github.com/coq/coq/archive/%PIN_COQ%.tar.gz" ^
+  -override-dev-pkg="coq=https://github.com/coq/coq/archive/%PIN_COQ%.tar.gz" ^
   || GOTO ErrorExit
 
 SET OPAMYES=yes
diff --git a/language-server/vscoq-language-server.opam b/language-server/vscoq-language-server.opam
index 24773c657..484f207b4 100644
--- a/language-server/vscoq-language-server.opam
+++ b/language-server/vscoq-language-server.opam
@@ -12,8 +12,8 @@ build: [
 ]
 depends: [
   "ocaml" { >= "4.13.1" }
-  "coq-core" { >= "8.18" < "8.19" }
-  "coq-stdlib" { >= "8.18" < "8.19" }
+  "coq-core" { = "dev" }
+  "coq-stdlib" { = "dev" }
   "yojson"
   "ocamlfind"
   "ppx_inline_test"

From b57c98a0b80b80cc6b38f69ca22568a3b67c421c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= <maxime.denes@inria.fr>
Date: Mon, 21 Aug 2023 16:32:23 +0200
Subject: [PATCH 02/31] Fix Nix build

---
 flake.lock | 20 ++++++++++----------
 flake.nix  |  2 +-
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/flake.lock b/flake.lock
index 897eaf40f..ad83cb877 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,17 +8,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1686065665,
-        "narHash": "sha256-a5QGrcqcPLNq/JgpWzXgkV5TrnuyGHcppsh86Ft+pbs=",
+        "lastModified": 1692621436,
+        "narHash": "sha256-fLkFHuL8vu4v7Oc9v2701d7pVM/eS/7mCJTEuAFfksA=",
         "owner": "coq",
         "repo": "coq",
-        "rev": "51814505fdeb5bc9f11fc7bd95493f0e7397509f",
+        "rev": "fbaea89860348ca2b2ca485e52df7215bea27746",
         "type": "github"
       },
       "original": {
         "owner": "coq",
-        "ref": "master",
         "repo": "coq",
+        "rev": "fbaea89860348ca2b2ca485e52df7215bea27746",
         "type": "github"
       }
     },
@@ -45,11 +45,11 @@
         "systems": "systems_2"
       },
       "locked": {
-        "lastModified": 1685518550,
-        "narHash": "sha256-o2d0KcvaXzTrPRIo0kOLV0/QXHhDQ5DTi+OxcjO8xqY=",
+        "lastModified": 1689068808,
+        "narHash": "sha256-6ixXo3wt24N/melDWjq70UuHQLxGV8jZvooRanIHXw0=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "a1720a10a6cfe8234c0e93907ffe81be440f4cef",
+        "rev": "919d646de7be200f3bf08cb76ae1f09402b6f9b4",
         "type": "github"
       },
       "original": {
@@ -60,11 +60,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1686058679,
-        "narHash": "sha256-TQ4IeSgKFDJb0uMaL89ujyEYW6Pppbk+I+UShH4DwXY=",
+        "lastModified": 1692494774,
+        "narHash": "sha256-noGVoOTyZ2Kr5OFglzKYOX48cx3hggdCPbXrYMG2FDw=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "6afc04d14fd5de5c03645e65ef227c2983d85d2a",
+        "rev": "3476a10478587dec90acb14ec6bde0966c545cc0",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 3c97eceb5..571070448 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,7 +5,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    coq-master = { url = "github:coq/coq/master/fbaea89860348ca2b2ca485e52df7215bea27746"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master = { url = "github:coq/coq/fbaea89860348ca2b2ca485e52df7215bea27746"; }; # Should be kept in sync with PIN_COQ in CI workflow
     coq-master.inputs.nixpkgs.follows = "nixpkgs";
 
   };

From a3b395613afea30071a088e5abf020622b32483b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 9 Aug 2023 16:56:06 +0200
Subject: [PATCH 03/31] Adapt to coq/coq#17928 (Search uses search_restriction
 instead of bool)

---
 language-server/dm/searchQuery.ml  | 16 ++--------------
 language-server/dm/searchQuery.mli |  2 +-
 2 files changed, 3 insertions(+), 15 deletions(-)

diff --git a/language-server/dm/searchQuery.ml b/language-server/dm/searchQuery.ml
index 92706e096..9cf543c5e 100644
--- a/language-server/dm/searchQuery.ml
+++ b/language-server/dm/searchQuery.ml
@@ -14,8 +14,7 @@
 open Util
 open Printer
 open Protocol.LspWrapper
-open Vernacexpr
-open Pp
+
 (* Note: this queue is not very useful today, as we process results in the main
 vscoq process, which does not allow for real asynchronous processing of results. *)
 let query_results_queue = Queue.create ()
@@ -24,17 +23,6 @@ let query_feedback : notification Sel.event =
   Sel.on_queue query_results_queue (fun x -> QueryResultNotification x)
   |> Sel.uncancellable
 
-(* TODO : remove these two functions when interp_search_restriction is 
-  added in the comSearch.mli in Coq (they're simply copied here for now) *)
-let global_module qid =
-    try Nametab.full_name_module qid
-    with Not_found ->  
-      CErrors.user_err ?loc:qid.CAst.loc
-       (str "Module/Section " ++ Ppconstr.pr_qualid qid ++ str " not found.")
-let interp_search_restriction = function
-  | SearchOutside l -> (List.map global_module l, true)
-  | SearchInside l -> (List.map global_module l, false)
-
 let interp_search ~id env sigma s r =
   let pr_search ref _kind env c =
     let pr = pr_global ref in
@@ -47,7 +35,7 @@ let interp_search ~id env sigma s r =
     let statement = Pp.string_of_ppcmds pc in
     Queue.push { id; name; statement } query_results_queue
   in
-  let r = interp_search_restriction r in
+  let r = ComSearch.interp_search_restriction r in
   (Search.search env sigma (List.map (ComSearch.interp_search_request env Evd.(from_env env)) s) r |>
     Search.prioritize_search) pr_search;
   [query_feedback]
diff --git a/language-server/dm/searchQuery.mli b/language-server/dm/searchQuery.mli
index 38e3dd663..87a1ffc54 100644
--- a/language-server/dm/searchQuery.mli
+++ b/language-server/dm/searchQuery.mli
@@ -20,5 +20,5 @@ val interp_search :
   Environ.env ->
   Evd.evar_map ->
   (bool * Vernacexpr.search_request) list ->
-  Vernacexpr.search_restriction ->
+  Libnames.qualid list Vernacexpr.search_restriction ->
   notification Sel.event list

From 5ee2ad46d7e16c6072bccebe52a75c6e858f262d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 30 Aug 2023 16:34:34 +0200
Subject: [PATCH 04/31] Adapt to Coq PR #17987 which adds sigma to the API of
 search functions

---
 language-server/dm/completionSuggester.ml | 4 ++--
 language-server/dm/searchQuery.ml         | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/language-server/dm/completionSuggester.ml b/language-server/dm/completionSuggester.ml
index f36f794c9..0de9a8bc9 100644
--- a/language-server/dm/completionSuggester.ml
+++ b/language-server/dm/completionSuggester.ml
@@ -418,10 +418,10 @@ let get_completion_items env proof lemmas options =
 let get_lemmas sigma env =
   let open CompletionItems in
   let results = ref [] in
-  let display ref _kind env c =
+  let display ref _kind env sigma c =
     results := mk_completion_item sigma ref env c :: results.contents;
   in
-  Search.generic_search env display;
+  Search.generic_search env sigma display;
   results.contents
 
 let get_completions options st =
diff --git a/language-server/dm/searchQuery.ml b/language-server/dm/searchQuery.ml
index 9cf543c5e..76cf2536e 100644
--- a/language-server/dm/searchQuery.ml
+++ b/language-server/dm/searchQuery.ml
@@ -24,18 +24,18 @@ let query_feedback : notification Sel.event =
   |> Sel.uncancellable
 
 let interp_search ~id env sigma s r =
-  let pr_search ref _kind env c =
+  let pr_search ref _kind env sigma c =
     let pr = pr_global ref in
     let open Impargs in
     let impls = implicits_of_global ref in
     let impargs = select_stronger_impargs impls in
     let impargs = List.map binding_kind_of_status impargs in
-    let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in
+    let pc = pr_ltype_env env sigma ~impargs c in
     let name = Pp.string_of_ppcmds pr in
     let statement = Pp.string_of_ppcmds pc in
     Queue.push { id; name; statement } query_results_queue
   in
   let r = ComSearch.interp_search_restriction r in
-  (Search.search env sigma (List.map (ComSearch.interp_search_request env Evd.(from_env env)) s) r |>
+  (Search.search env sigma (List.map (ComSearch.interp_search_request env sigma) s) r |>
     Search.prioritize_search) pr_search;
   [query_feedback]

From de88278e02831707d919fe4bf8b29524230e192d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 8 Oct 2023 16:11:32 +0200
Subject: [PATCH 05/31] Adapt to Coq PR #18007: Proof_using.definition_using
 takes names of recursive definitions as extra arguments.

---
 language-server/dm/executionManager.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 351f0eb96..4a8a21277 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -188,8 +188,10 @@ let interp_qed_delayed ~proof_using ~state_id ~st =
       let env = Global.env () in
       let sigma, _ = Declare.Proof.get_current_context proof in
       let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
-      let terms = List.map (fun (_,_,x) -> x) (initial_goals (Declare.Proof.get proof)) in
-      let using = Proof_using.definition_using env sigma ~using:proof_using ~terms in
+      let initial_goals_pf = initial_goals (Declare.Proof.get proof) in
+      let terms = List.map (fun (_,_,x) -> x) initial_goals_pf in
+      let names = List.map (fun (id,_,_) -> id) initial_goals_pf in
+      let using = Proof_using.definition_using env sigma ~fixnames:names ~using:proof_using ~terms in
       let vars = Environ.named_context env in
       Names.Id.Set.iter (fun id ->
           if not (List.exists Util.(Context.Named.Declaration.get_id %> Names.Id.equal id) vars) then

From 4e6a8552dbe27888d6f6c39fcc435230384519f0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 8 Oct 2023 16:23:07 +0200
Subject: [PATCH 06/31] Adapt to Coq PR #18007: Proof_using.definition_using
 takes names of recursive definitions as extra arguments.

---
 language-server/dm/executionManager.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 4a8a21277..0246a0721 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -183,14 +183,14 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast =
 
 (* This adapts the Future API with our event model *)
 let interp_qed_delayed ~proof_using ~state_id ~st =
+  let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in
   let f proof =
     let proof =
       let env = Global.env () in
       let sigma, _ = Declare.Proof.get_current_context proof in
       let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
-      let initial_goals_pf = initial_goals (Declare.Proof.get proof) in
-      let terms = List.map (fun (_,_,x) -> x) initial_goals_pf in
-      let names = List.map (fun (id,_,_) -> id) initial_goals_pf in
+      let terms = List.map (fun (_,_,x) -> x) (initial_goals (Declare.Proof.get proof)) in
+      let names = Vernacstate.LemmaStack.get_all_proof_names lemmas in
       let using = Proof_using.definition_using env sigma ~fixnames:names ~using:proof_using ~terms in
       let vars = Environ.named_context env in
       Names.Id.Set.iter (fun id ->
@@ -204,7 +204,6 @@ let interp_qed_delayed ~proof_using ~state_id ~st =
     let f, assign = Future.create_delegate ~blocking:false ~name:"XX" fix_exn in
     Declare.Proof.close_future_proof ~feedback_id:state_id proof f, assign
   in
-  let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in
   let proof, assign = Vernacstate.LemmaStack.with_top lemmas ~f in
   let control = [] (* FIXME *) in
   let opaque = Vernacexpr.Opaque in

From 5f750adfef88ab34a93c38842bee79078f6a21a7 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 9 Oct 2023 15:47:18 +0200
Subject: [PATCH 07/31] Adapt to https://github.com/coq/coq/pull/14928

---
 language-server/language/hover.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/language-server/language/hover.ml b/language-server/language/hover.ml
index 1d935a7ef..ef2b34bde 100644
--- a/language-server/language/hover.ml
+++ b/language-server/language/hover.ml
@@ -40,7 +40,11 @@ let compactify s =
 (* TODO this should be exposed by Coq and removed from here *)
 let pr_args args more_implicits mods =
   let open Vernacexpr in
-  let pr_s = prlist (fun CAst.{v=s} -> str "%" ++ str s) in
+  let pr_delimiter_depth = function
+    | Constrexpr.DelimOnlyTmpScope -> str "%_"
+    | Constrexpr.DelimUnboundedScope -> str "%" in
+  let pr_scope_delimiter (d, sc) = pr_delimiter_depth d ++ str sc in
+  let pr_s = prlist (fun CAst.{v=s} -> pr_scope_delimiter s) in
   let pr_if b x = if b then x else str "" in
   let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in
   let pr_br imp force x =
@@ -57,7 +61,9 @@ let pr_args args more_implicits mods =
     else
       let rec fold extra = function
         | RealArg arg :: tl when
-            List.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s
+            List.equal
+              (fun a b -> let da, a = a.CAst.v in let db, b = b.CAst.v in
+               da = db && String.equal a b) arg.notation_scope s
             && arg.implicit_status = imp ->
           fold ((arg.name,arg.recarg_like) :: extra) tl
         | args -> List.rev extra, args
@@ -131,7 +137,7 @@ let rec main_implicits i renames recargs scopes impls =
       | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit)
     in
     let notation_scope = match scopes with
-      | scope :: _ -> List.map CAst.make scope
+      | scope :: _ -> List.map (fun s -> CAst.make (Constrexpr.DelimUnboundedScope, s)) scope
       | [] -> []
     in
     let status = {Vernacexpr.implicit_status; name; recarg_like; notation_scope} in
@@ -260,4 +266,4 @@ let get_hover_contents env sigma ref_or_by_not =
     end
     in
     Option.map Lsp.Types.(fun value -> MarkupContent.create ~kind:MarkupKind.Markdown ~value) r
-  | Constrexpr.ByNotation (_ntn,_sc) -> assert false
\ No newline at end of file
+  | Constrexpr.ByNotation (_ntn,_sc) -> assert false

From b3a7ed9c73fe2c8a598cebae6865d5c562f64374 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 24 Oct 2023 13:54:21 +0200
Subject: [PATCH 08/31] Adapt to coq/coq#18187 (reductionbehaviour is on
 constant not globref)

---
 language-server/language/hover.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/language-server/language/hover.ml b/language-server/language/hover.ml
index 1d935a7ef..49db09890 100644
--- a/language-server/language/hover.ml
+++ b/language-server/language/hover.ml
@@ -169,11 +169,15 @@ let rec insert_fake_args volatile bidi impls =
 let print_arguments ref =
   let flags, recargs, nargs_for_red =
     let open Reductionops.ReductionBehaviour in
-    match get ref with
-    | None -> [], [], None
-    | Some NeverUnfold -> [`ReductionNeverUnfold], [], None
-    | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs
-    | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs
+    match ref with
+    | GlobRef.ConstRef ref ->
+      begin match get ref with
+      | None -> [], [], None
+      | Some NeverUnfold -> [`ReductionNeverUnfold], [], None
+      | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs
+      | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs
+      end
+    | _ -> [], [], None
   in
   let names, not_renamed =
     try Arguments_renaming.arguments_names ref, false
@@ -260,4 +264,4 @@ let get_hover_contents env sigma ref_or_by_not =
     end
     in
     Option.map Lsp.Types.(fun value -> MarkupContent.create ~kind:MarkupKind.Markdown ~value) r
-  | Constrexpr.ByNotation (_ntn,_sc) -> assert false
\ No newline at end of file
+  | Constrexpr.ByNotation (_ntn,_sc) -> assert false

From 52e93f51bdadd8c9ce33693e5d0be548957c14db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Mon, 6 Nov 2023 10:59:21 +0100
Subject: [PATCH 09/31] Adapt w.r.t. coq/coq#17136.

---
 language-server/dm/document.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
index 5bc35c561..d99c4d7e1 100644
--- a/language-server/dm/document.ml
+++ b/language-server/dm/document.ml
@@ -278,7 +278,7 @@ let rec parse_more synterp_state stream raw parsed errors =
           let loc = Loc.get_loc @@ info in
           handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info))
         end
-    | exception (Stream.Error msg as exn) ->
+    | exception (Grammar.Error msg as exn) ->
       let loc = Loc.get_loc @@ Exninfo.info exn in
       junk_sentence_end stream;
       handle_parse_error start (loc,msg)
@@ -375,4 +375,4 @@ module Internal = struct
     sentence.start
     sentence.stop
 
-end
\ No newline at end of file
+end

From a1aa8fe3f798959a634ed18721b0667cc21634ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Wed, 15 Nov 2023 12:44:01 +0100
Subject: [PATCH 10/31] Adapt w.r.t. coq/coq#18312.

---
 language-server/language/hover.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/language-server/language/hover.ml b/language-server/language/hover.ml
index 2341b9a9b..82bf83410 100644
--- a/language-server/language/hover.ml
+++ b/language-server/language/hover.ml
@@ -105,7 +105,9 @@ let pr_args args more_implicits mods =
 
 let implicit_kind_of_status = function
   | None -> Anonymous, Glob_term.Explicit
-  | Some ((na,_,_),_,(maximal,_)) -> na, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
+  | Some imp ->
+    let (na, _, _) = imp.Impargs.impl_pos in
+    na, if imp.Impargs.impl_max then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
 
 let extra_implicit_kind_of_status imp =
   let _,imp = implicit_kind_of_status imp in

From 0dba89aa7e3694be78f6249c38400e07b06364b0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 24 Dec 2023 14:24:35 +0100
Subject: [PATCH 11/31] [ci] opam: test 8.18 and 8.19

---
 .github/workflows/ci.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 4d9ddf174..8d37d75c9 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -58,6 +58,7 @@ jobs:
       matrix:
         os: [ubuntu-latest]
         ocaml-compiler: [4.13.x]
+        coq: [8.18.0, 8.19+rc1]
     runs-on: ${{ matrix.os }}
     steps:
     - name: Checkout
@@ -73,6 +74,7 @@ jobs:
         OPAMYES: true
       run: |
         opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
+        opam pin add coq-core.${{ matrix.coq }}
         opam pin add vscoq-language-server ./language-server/ --with-doc --with-test -y
 
     - run: |

From 215b5e10bee2c075aacea270ac6c1c07b6266d9b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 24 Dec 2023 15:49:47 +0100
Subject: [PATCH 12/31] [ppx_optcomp] define coq version

---
 language-server/dm/dune                    | 1 +
 language-server/dune-project               | 3 ++-
 language-server/language/dune              | 1 +
 language-server/vscoq-language-server.opam | 3 ++-
 4 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/language-server/dm/dune b/language-server/dm/dune
index 4dc1c7f49..151794fa5 100644
--- a/language-server/dm/dune
+++ b/language-server/dm/dune
@@ -2,6 +2,7 @@
  (name dm)
  (public_name vscoq-language-server.dm)
  (modules :standard \ vscoqtop_proof_worker vscoqtop_tactic_worker)
+ (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
  (libraries base coq-core.sysinit coq-core.vernac coq-core.parsing lsp sel protocol language))
 
 (executable
diff --git a/language-server/dune-project b/language-server/dune-project
index 6f43ab3fd..74ee14d86 100644
--- a/language-server/dune-project
+++ b/language-server/dune-project
@@ -1,4 +1,5 @@
-(lang dune 3.2)
+(lang dune 3.5)
+(using coq 0.6)
 (name vscoq-language-server)
 (license LGPL-2.1-only)
 (authors "The VsCoq development team")
diff --git a/language-server/language/dune b/language-server/language/dune
index aad9afdda..5c69f412e 100644
--- a/language-server/language/dune
+++ b/language-server/language/dune
@@ -1,4 +1,5 @@
 (library
  (name language)
  (public_name vscoq-language-server.language)
+ (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
  (libraries coq-core.sysinit lsp))
\ No newline at end of file
diff --git a/language-server/vscoq-language-server.opam b/language-server/vscoq-language-server.opam
index ba508be1e..5bcb22b77 100644
--- a/language-server/vscoq-language-server.opam
+++ b/language-server/vscoq-language-server.opam
@@ -12,7 +12,7 @@ build: [
 ]
 depends: [
   "ocaml" { >= "4.13.1" }
-  "dune" { >= "3.2" }
+  "dune" { >= "3.5" }
   "coq-core" { >= "8.18" < "8.19" }
   "coq-stdlib" { >= "8.18" < "8.19" }
   "yojson"
@@ -26,6 +26,7 @@ depends: [
   "sexplib"
   "ppx_yojson_conv"
   "ppx_import"
+  "ppx_optcomp"
   "result" { >= "1.5" }
   "lsp" { >= "1.15"}
   "sel" {>= "0.4.0"}

From 3e737ce30814232e60d92ae3324fc3a2865d068b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 24 Dec 2023 15:50:22 +0100
Subject: [PATCH 13/31] [wip] ifdef for 8.18

---
 language-server/language/hover.ml | 53 ++++++++++++++++++++++---------
 1 file changed, 38 insertions(+), 15 deletions(-)

diff --git a/language-server/language/hover.ml b/language-server/language/hover.ml
index 4afbf1d2d..6b4426e7b 100644
--- a/language-server/language/hover.ml
+++ b/language-server/language/hover.ml
@@ -38,13 +38,31 @@ let compactify s =
   List.fold_left (fun s (reg,repl) -> Str.global_replace reg repl s) s replacements
 
 (* TODO this should be exposed by Coq and removed from here *)
+
+[%%if coq = "8.18"]
+let pr_s = prlist (fun CAst.{v=s} -> str "%" ++ str s)
+let eq_realarg = List.equal (fun a b -> String.equal a.CAst.v b.CAst.v)
+let nargs_maximal_of_pos ((na,_,_),_,(maximal,_)) = na, maximal
+let make_scope = CAst.make
+[%%else]
+let pr_delimiter_depth = function
+  | Constrexpr.DelimOnlyTmpScope -> str "%_"
+  | Constrexpr.DelimUnboundedScope -> str "%"
+let pr_scope_delimiter (d, sc) = pr_delimiter_depth d ++ str sc
+let pr_s = prlist (fun CAst.{v=s} -> pr_scope_delimiter s)
+
+let eq_realarg =
+  List.equal
+   (fun a b -> let da, a = a.CAst.v in let db, b = b.CAst.v in
+    da = db && String.equal a b)
+let nargs_of_pos imp =
+  let (na, _, _) = imp.Impargs.impl_pos in
+  na, imp.Impargs.impl_max
+let make_scope = (fun s -> CAst.make (Constrexpr.DelimUnboundedScope, s))
+[%%endif]
+
 let pr_args args more_implicits mods =
   let open Vernacexpr in
-  let pr_delimiter_depth = function
-    | Constrexpr.DelimOnlyTmpScope -> str "%_"
-    | Constrexpr.DelimUnboundedScope -> str "%" in
-  let pr_scope_delimiter (d, sc) = pr_delimiter_depth d ++ str sc in
-  let pr_s = prlist (fun CAst.{v=s} -> pr_scope_delimiter s) in
   let pr_if b x = if b then x else str "" in
   let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in
   let pr_br imp force x =
@@ -60,10 +78,7 @@ let pr_args args more_implicits mods =
     if s = [] && imp = Glob_term.Explicit then [], tl
     else
       let rec fold extra = function
-        | RealArg arg :: tl when
-            List.equal
-              (fun a b -> let da, a = a.CAst.v in let db, b = b.CAst.v in
-               da = db && String.equal a b) arg.notation_scope s
+        | RealArg arg :: tl when eq_realarg arg.notation_scope s
             && arg.implicit_status = imp ->
           fold ((arg.name,arg.recarg_like) :: extra) tl
         | args -> List.rev extra, args
@@ -106,8 +121,8 @@ let pr_args args more_implicits mods =
 let implicit_kind_of_status = function
   | None -> Anonymous, Glob_term.Explicit
   | Some imp ->
-    let (na, _, _) = imp.Impargs.impl_pos in
-    na, if imp.Impargs.impl_max then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
+    let na, maximal = nargs_maximal_of_pos imp in
+    na, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
 
 let extra_implicit_kind_of_status imp =
   let _,imp = implicit_kind_of_status imp in
@@ -139,7 +154,7 @@ let rec main_implicits i renames recargs scopes impls =
       | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit)
     in
     let notation_scope = match scopes with
-      | scope :: _ -> List.map (fun s -> CAst.make (Constrexpr.DelimUnboundedScope, s)) scope
+      | scope :: _ -> List.map make_scope scope
       | [] -> []
     in
     let status = {Vernacexpr.implicit_status; name; recarg_like; notation_scope} in
@@ -174,18 +189,26 @@ let rec insert_fake_args volatile bidi impls =
     let f = Option.map pred in
     RealArg hd :: insert_fake_args (f volatile) (f bidi) tl
 
+[%%if coq = "8.18"]
+let ref_of_const x = Some x
+[%%else]
+let ref_of_const = function
+| GlobRef.ConstRef ref -> Some ref
+| _ -> None
+[%%endif]
+
 let print_arguments ref =
   let flags, recargs, nargs_for_red =
     let open Reductionops.ReductionBehaviour in
-    match ref with
-    | GlobRef.ConstRef ref ->
+    match ref_of_const ref with
+    | Some ref ->
       begin match get ref with
       | None -> [], [], None
       | Some NeverUnfold -> [`ReductionNeverUnfold], [], None
       | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs
       | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs
       end
-    | _ -> [], [], None
+    | None -> [], [], None
   in
   let names, not_renamed =
     try Arguments_renaming.arguments_names ref, false

From ca7733b320f09f6c7f578a7ee3fd38aa3799a435 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 24 Dec 2023 15:55:00 +0100
Subject: [PATCH 14/31] downgrade dune, there is an error with lang dune 3.5

---
 language-server/dune-project | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/language-server/dune-project b/language-server/dune-project
index 74ee14d86..6f43ab3fd 100644
--- a/language-server/dune-project
+++ b/language-server/dune-project
@@ -1,5 +1,4 @@
-(lang dune 3.5)
-(using coq 0.6)
+(lang dune 3.2)
 (name vscoq-language-server)
 (license LGPL-2.1-only)
 (authors "The VsCoq development team")

From 1c3e1f2e47e52e7687d6019d5c364a12a365d396 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Sun, 24 Dec 2023 16:00:29 +0100
Subject: [PATCH 15/31] Update .github/workflows/ci.yml

---
 .github/workflows/ci.yml | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8d37d75c9..cd3350861 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -136,13 +136,6 @@ jobs:
       with:
         ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
-    - name: Pin Coq
-      env:
-        OPAMYES: true
-      run: |
-        opam pin add coq-core.dev "https://github.com/coq/coq.git#$PIN_COQ"
-        opam pin add coq-stdlib.dev "https://github.com/coq/coq.git#$PIN_COQ"
-
     - name: Install deps
       env:
         OPAMYES: true

From 58a8df2c68205fec664904c3bd819b2da344e943 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Sun, 24 Dec 2023 16:00:55 +0100
Subject: [PATCH 16/31] Update .github/workflows/ci.yml

---
 .github/workflows/ci.yml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index cd3350861..3e5936107 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -6,9 +6,6 @@ on:
   pull_request:
   workflow_dispatch:
 
-env:
-  PIN_COQ: fbaea89860348ca2b2ca485e52df7215bea27746 # Should be kept in sync with input in flake.nix
-
 jobs:
   build-extension:
     strategy:

From 9284071e6fbdbe01a6debaaa36145cfe30f62671 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Sun, 24 Dec 2023 16:01:50 +0100
Subject: [PATCH 17/31] Update language-server/build-windows-platform.bat

---
 language-server/build-windows-platform.bat | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/language-server/build-windows-platform.bat b/language-server/build-windows-platform.bat
index 3716033a5..01d531fa7 100644
--- a/language-server/build-windows-platform.bat
+++ b/language-server/build-windows-platform.bat
@@ -31,9 +31,9 @@ call coq_platform_make_windows.bat ^
   -jobs=2 ^
   -switch=d ^
   -set-switch=y ^
-  -override-dev-pkg="coq-core=https://github.com/coq/coq/archive/%PIN_COQ%.tar.gz" ^
-  -override-dev-pkg="coq-stdlib=https://github.com/coq/coq/archive/%PIN_COQ%.tar.gz" ^
-  -override-dev-pkg="coq=https://github.com/coq/coq/archive/%PIN_COQ%.tar.gz" ^
+  -override-dev-pkg="coq-core=https://github.com/coq/coq/archive/%COQ_VERSION%.tar.gz" ^
+  -override-dev-pkg="coq-stdlib=https://github.com/coq/coq/archive/%COQ_VERSION%.tar.gz" ^
+  -override-dev-pkg="coq=https://github.com/coq/coq/archive/%COQ_VERSION%.tar.gz" ^
   || GOTO ErrorExit
 
 SET OPAMYES=yes

From 9c8a869ec3474918dfa95e58094c93c2bf58ee04 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 24 Dec 2023 16:13:01 +0100
Subject: [PATCH 18/31] fixup ci

---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3e5936107..e35819f5a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -71,7 +71,7 @@ jobs:
         OPAMYES: true
       run: |
         opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-        opam pin add coq-core.${{ matrix.coq }}
+        opam pin add coq-core ${{ matrix.coq }}
         opam pin add vscoq-language-server ./language-server/ --with-doc --with-test -y
 
     - run: |

From 3a9f22968ae177f0db4bf6644b68a42c5662b74c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 24 Dec 2023 17:33:37 +0100
Subject: [PATCH 19/31] fix ci opam

---
 .github/workflows/ci.yml                   | 1 +
 language-server/vscoq-language-server.opam | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e35819f5a..f9357e950 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -52,6 +52,7 @@ jobs:
 
   install-opam:
     strategy:
+      fail-fast: false
       matrix:
         os: [ubuntu-latest]
         ocaml-compiler: [4.13.x]
diff --git a/language-server/vscoq-language-server.opam b/language-server/vscoq-language-server.opam
index 5bcb22b77..9a7e05c9b 100644
--- a/language-server/vscoq-language-server.opam
+++ b/language-server/vscoq-language-server.opam
@@ -13,8 +13,8 @@ build: [
 depends: [
   "ocaml" { >= "4.13.1" }
   "dune" { >= "3.5" }
-  "coq-core" { >= "8.18" < "8.19" }
-  "coq-stdlib" { >= "8.18" < "8.19" }
+  "coq-core" { >= "8.18" < "8.20" }
+  "coq-stdlib" { >= "8.18" < "8.20" }
   "yojson"
   "jsonrpc" { >= "1.15"}
   "ocamlfind"

From 466e73206cf4346a4b29f1516c8b6eb13116f53a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sun, 24 Dec 2023 21:42:47 +0100
Subject: [PATCH 20/31] progress

---
 language-server/dm/searchQuery.mli | 10 ++++++++++
 language-server/language/hover.ml  |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/language-server/dm/searchQuery.mli b/language-server/dm/searchQuery.mli
index dafc00bd8..e44a51087 100644
--- a/language-server/dm/searchQuery.mli
+++ b/language-server/dm/searchQuery.mli
@@ -15,6 +15,15 @@ open Protocol.LspWrapper
 
 val query_feedback : notification Sel.Event.t
 
+[%%if coq = "8.18"]
+val interp_search :
+  id:string ->
+  Environ.env ->
+  Evd.evar_map ->
+  (bool * Vernacexpr.search_request) list ->
+  Vernacexpr.search_restriction ->
+  notification Sel.Event.t list
+[%%else]
 val interp_search :
   id:string ->
   Environ.env ->
@@ -22,3 +31,4 @@ val interp_search :
   (bool * Vernacexpr.search_request) list ->
   Libnames.qualid list Vernacexpr.search_restriction ->
   notification Sel.Event.t list
+[%%endif]
diff --git a/language-server/language/hover.ml b/language-server/language/hover.ml
index 6b4426e7b..ec205be80 100644
--- a/language-server/language/hover.ml
+++ b/language-server/language/hover.ml
@@ -55,7 +55,7 @@ let eq_realarg =
   List.equal
    (fun a b -> let da, a = a.CAst.v in let db, b = b.CAst.v in
     da = db && String.equal a b)
-let nargs_of_pos imp =
+let nargs_maximal_of_pos imp =
   let (na, _, _) = imp.Impargs.impl_pos in
   na, imp.Impargs.impl_max
 let make_scope = (fun s -> CAst.make (Constrexpr.DelimUnboundedScope, s))

From 355e0dd2fe54b9d2b68edc63a331cc6a6e9eba4b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 25 Dec 2023 14:31:08 +0100
Subject: [PATCH 21/31] fix more code

---
 language-server/dm/completionSuggester.ml |  7 ++++++-
 language-server/dm/executionManager.ml    |  9 ++++++++-
 language-server/dm/searchQuery.ml         | 23 +++++++++++++++++++++--
 3 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/language-server/dm/completionSuggester.ml b/language-server/dm/completionSuggester.ml
index 0de9a8bc9..ecdd40391 100644
--- a/language-server/dm/completionSuggester.ml
+++ b/language-server/dm/completionSuggester.ml
@@ -415,13 +415,18 @@ let get_completion_items env proof lemmas options =
     log ("Ranking of lemmas failed: " ^ (Printexc.to_string e));
     lemmas
 
+[%%if coq = "8.18"]
+let generic_search e s f = Search.generic_search e (fun r k e c -> f r k e s c)
+[%%else]
+let generic_search = Search.generic_search
+[%%endif]
 let get_lemmas sigma env =
   let open CompletionItems in
   let results = ref [] in
   let display ref _kind env sigma c =
     results := mk_completion_item sigma ref env c :: results.contents;
   in
-  Search.generic_search env sigma display;
+  generic_search env sigma display;
   results.contents
 
 let get_completions options st =
diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 2ac57a691..c2f51f18a 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -182,6 +182,13 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast =
         st, status, []
 
 (* This adapts the Future API with our event model *)
+[%%if coq = "8.18"]
+let definition_using e s ~fixnames:_ ~using ~terms =
+  Proof_using.definition_using e s ~using ~terms
+
+[%%else]
+let definition_using = Proof_using.definition_using
+[%%endif]
 let interp_qed_delayed ~proof_using ~state_id ~st =
   let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in
   let f proof =
@@ -191,7 +198,7 @@ let interp_qed_delayed ~proof_using ~state_id ~st =
       let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
       let terms = List.map (fun (_,_,x) -> x) (initial_goals (Declare.Proof.get proof)) in
       let names = Vernacstate.LemmaStack.get_all_proof_names lemmas in
-      let using = Proof_using.definition_using env sigma ~fixnames:names ~using:proof_using ~terms in
+      let using = definition_using env sigma ~fixnames:names ~using:proof_using ~terms in
       let vars = Environ.named_context env in
       Names.Id.Set.iter (fun id ->
           if not (List.exists Util.(Context.Named.Declaration.get_id %> Names.Id.equal id) vars) then
diff --git a/language-server/dm/searchQuery.ml b/language-server/dm/searchQuery.ml
index 856dcd364..803f2789a 100644
--- a/language-server/dm/searchQuery.ml
+++ b/language-server/dm/searchQuery.ml
@@ -23,6 +23,25 @@ let query_results_queue = Queue.create ()
 let query_feedback : notification Sel.Event.t =
   Sel.On.queue query_results_queue (fun x -> QueryResultNotification x)
 
+[%%if coq = "8.18"]
+open Vernacexpr
+open Pp
+(* TODO : remove these two functions when interp_search_restriction is 
+  added in the comSearch.mli in Coq (they're simply copied here for now) *)
+let global_module qid =
+    try Nametab.full_name_module qid
+    with Not_found ->  
+      CErrors.user_err ?loc:qid.CAst.loc
+       (str "Module/Section " ++ Ppconstr.pr_qualid qid ++ str " not found.")
+let interp_search_restriction = function
+  | SearchOutside l -> (List.map global_module l, true)
+  | SearchInside l -> (List.map global_module l, false)
+let adapt_pr_search f r k e c = f r k e (Evd.from_env e) c
+[%%else]
+let interp_search_restriction = ComSearch.interp_search_restriction
+let adapt_pr_search f = f
+[%%endif]
+
 let interp_search ~id env sigma s r =
   let pr_search ref _kind env sigma c =
     let pr = pr_global ref in
@@ -35,7 +54,7 @@ let interp_search ~id env sigma s r =
     let statement = pp_of_coqpp pc in
     Queue.push { id; name; statement } query_results_queue
   in
-  let r = ComSearch.interp_search_restriction r in
+  let r = interp_search_restriction r in
   (Search.search env sigma (List.map (ComSearch.interp_search_request env sigma) s) r |>
-    Search.prioritize_search) pr_search;
+    Search.prioritize_search) (adapt_pr_search pr_search);
   [query_feedback]

From f40ef2911dc5ea11e112bbc5cf53c30c3705c313 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 25 Dec 2023 16:07:08 +0100
Subject: [PATCH 22/31] more fix

---
 language-server/dm/document.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
index c25f73c38..edda41a5f 100644
--- a/language-server/dm/document.ml
+++ b/language-server/dm/document.ml
@@ -252,6 +252,12 @@ let rec junk_sentence_end stream =
   | [] -> ()
   | _ ->  Stream.junk () stream; junk_sentence_end stream
 
+[%%if coq = "8.18"]
+exception E = Stream.Error
+[%%else]
+exception E = Grammar.Error
+[%%endif]
+
 let rec parse_more synterp_state stream raw parsed errors =
   let handle_parse_error start msg =
     log @@ "handling parse error at " ^ string_of_int start;
@@ -290,7 +296,7 @@ let rec parse_more synterp_state stream raw parsed errors =
           let loc = Loc.get_loc @@ info in
           handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info))
         end
-    | exception (Grammar.Error msg as exn) ->
+    | exception (E msg as exn) ->
       let loc = Loc.get_loc @@ Exninfo.info exn in
       junk_sentence_end stream;
       handle_parse_error start (loc,msg)

From e1e89f4806880e1ed230d809b0b08b9a00ab790d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 29 Dec 2023 16:49:37 +0100
Subject: [PATCH 23/31] Update language-server/dm/executionManager.ml

---
 language-server/dm/executionManager.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index c2f51f18a..1ad132958 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -185,7 +185,6 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast =
 [%%if coq = "8.18"]
 let definition_using e s ~fixnames:_ ~using ~terms =
   Proof_using.definition_using e s ~using ~terms
-
 [%%else]
 let definition_using = Proof_using.definition_using
 [%%endif]

From c8f063ff25a317d25b7ab7c45046b720eb9188e9 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Tue, 30 Jan 2024 09:30:15 +0100
Subject: [PATCH 24/31] Updating nix flakes

---
 flake.nix | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/flake.nix b/flake.nix
index 747b38ee2..1709062f7 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,7 +5,6 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-<<<<<<< HEAD
     coq-8_18 = {
       type = "github";
       owner = "coq";
@@ -13,18 +12,22 @@
       ref = "V8.18.0";
     };
 
+    coq-8_19 = {
+      type = "github";
+      owner = "coq";
+      repo = "coq";
+      ref = "V8.19.0";
+    };
+
     coq-8_18.inputs.nixpkgs.follows = "nixpkgs";
-=======
-    coq-master = { url = "github:coq/coq/fbaea89860348ca2b2ca485e52df7215bea27746"; }; # Should be kept in sync with PIN_COQ in CI workflow
-    coq-master.inputs.nixpkgs.follows = "nixpkgs";
->>>>>>> coq-master
+    coq-8_19.inputs.nixpkgs.follows = "nixpkgs";
 
   };
 
-  outputs = { self, nixpkgs, flake-utils, coq-8_18 }:
+  outputs = { self, nixpkgs, flake-utils, coq-8_19 }:
     flake-utils.lib.eachDefaultSystem (system:
   
-   let coq = coq-8_18.defaultPackage.${system}; in
+   let coq = coq-8_19.defaultPackage.${system}; in
    rec {
 
     packages.default = self.packages.${system}.vscoq-language-server;

From 88787744dafe9a3305128cd0f41223ece56bc1aa Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Wed, 31 Jan 2024 21:00:38 +0100
Subject: [PATCH 25/31] fixing deps. wip

---
 flake.nix | 1 +
 1 file changed, 1 insertion(+)

diff --git a/flake.nix b/flake.nix
index f8680278e..247665dc0 100644
--- a/flake.nix
+++ b/flake.nix
@@ -39,6 +39,7 @@
           ppx_assert
           ppx_sexp_conv
           ppx_deriving
+          ppx_optcomp
           ppx_import
           sexplib
           ppx_yojson_conv

From 4b986bf598154a79a22332804fd0c0dbbe3b6ece Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Fri, 2 Feb 2024 09:28:42 +0100
Subject: [PATCH 26/31] Fixing nix.

---
 flake.nix | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/flake.nix b/flake.nix
index 247665dc0..dde838278 100644
--- a/flake.nix
+++ b/flake.nix
@@ -62,7 +62,20 @@
 
     };
 
-    devShells.default =
+    devShells.vscoq-client = 
+      with import nixpkgs { inherit system; };
+      mkShell {
+        buildInputs = self.packages.${system}.vscoq-client.buildInputs;
+      };
+
+    devShells.vscoq-language-server = 
+      with import nixpkgs { inherit system; };
+      mkShell {
+        buildInputs =
+          self.packages.${system}.vscoq-language-server.buildInputs;
+      };
+
+    devShells.default = 
       with import nixpkgs { inherit system; };
       mkShell {
         buildInputs =

From 9b99cb63232d74b15d2ef877415a3bbed3d357c9 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Mon, 5 Feb 2024 16:48:20 +0100
Subject: [PATCH 27/31] Nix build for different coq versions.

Make devShells for coq 8.18, coq 8.19 and coq master.
Run them all in the CI.
---
 .github/workflows/ci.yml |  3 +-
 flake.lock               | 58 +++++++++++++++++++++++-
 flake.nix                | 98 +++++++++++++++++++++++++++++++++++++---
 3 files changed, 151 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f11bee349..396c2dfd8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -27,6 +27,7 @@ jobs:
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]
+        coq: [coq-8-18, coq-8-19, coq-master]
     runs-on: ${{ matrix.os }}
     steps:
     - name: Checkout
@@ -41,7 +42,7 @@ jobs:
     - uses: cachix/install-nix-action@v22
       with:
         nix_path: nixpkgs=channel:nixos-unstable
-    - run: nix develop .#vscoq-language-server -c bash -c "cd language-server && dune build"
+    - run: nix develop .#vscoq-language-server-${{ matrix.coq }} -c bash -c "cd language-server && dune build"
     - run: nix develop .#vscoq-client -c bash -c "cd client && yarn run install:all && yarn run build:all && yarn run compile"
     - run: xvfb-run nix develop .#vscoq-client -c bash -c "cd client && yarn test"
       if: runner.os == 'Linux'
diff --git a/flake.lock b/flake.lock
index cb783bbf3..3f6eb2ac5 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,9 +1,49 @@
 {
   "nodes": {
+    "coq-master": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1692621436,
+        "narHash": "sha256-fLkFHuL8vu4v7Oc9v2701d7pVM/eS/7mCJTEuAFfksA=",
+        "owner": "coq",
+        "repo": "coq",
+        "rev": "fbaea89860348ca2b2ca485e52df7215bea27746",
+        "type": "github"
+      },
+      "original": {
+        "owner": "coq",
+        "repo": "coq",
+        "rev": "fbaea89860348ca2b2ca485e52df7215bea27746",
+        "type": "github"
+      }
+    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
       },
+      "locked": {
+        "lastModified": 1681202837,
+        "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "cfacdce06f30d2b68473a46042957675eebb3401",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "flake-utils_2": {
+      "inputs": {
+        "systems": "systems_2"
+      },
       "locked": {
         "lastModified": 1705309234,
         "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=",
@@ -34,7 +74,8 @@
     },
     "root": {
       "inputs": {
-        "flake-utils": "flake-utils",
+        "coq-master": "coq-master",
+        "flake-utils": "flake-utils_2",
         "nixpkgs": "nixpkgs"
       }
     },
@@ -52,6 +93,21 @@
         "repo": "default",
         "type": "github"
       }
+    },
+    "systems_2": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
     }
   },
   "root": "root",
diff --git a/flake.nix b/flake.nix
index dde838278..21c90383b 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,16 +5,88 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
+    coq-master = { url = "github:coq/coq/fbaea89860348ca2b2ca485e52df7215bea27746"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master.inputs.nixpkgs.follows = "nixpkgs";
+
   };
 
-  outputs = { self, nixpkgs, flake-utils }:
+  outputs = { self, nixpkgs, flake-utils, coq-master }:
     flake-utils.lib.eachDefaultSystem (system:
   
+   let coq = coq-master.defaultPackage.${system}; in
    rec {
 
-    packages.default = self.packages.${system}.vscoq-language-server;
+    packages.default = self.packages.${system}.vscoq-language-server-coq-8-19;
 
-    packages.vscoq-language-server =
+    packages.vscoq-language-server-coq-8-18 =
+      # Notice the reference to nixpkgs here.
+      with import nixpkgs { inherit system; };
+      let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in
+      ocamlPackages.buildDunePackage {
+        duneVersion = "3";
+        pname = "vscoq-language-server";
+        version = "2.0.3";
+        src = ./language-server;
+        buildInputs = [
+          coq_8_18
+          dune_3
+        ] ++ (with coq.ocamlPackages; [
+          lablgtk3-sourceview3
+          glib
+          gnome.adwaita-icon-theme
+          wrapGAppsHook
+          ocaml
+          yojson
+          zarith
+          findlib
+          ppx_inline_test
+          ppx_assert
+          ppx_sexp_conv
+          ppx_deriving
+          ppx_optcomp
+          ppx_import
+          sexplib
+          ppx_yojson_conv
+          lsp
+          sel
+        ]);
+      };
+
+      packages.vscoq-language-server-coq-8-19 =
+      # Notice the reference to nixpkgs here.
+      with import nixpkgs { inherit system; };
+      let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in
+      ocamlPackages.buildDunePackage {
+        duneVersion = "3";
+        pname = "vscoq-language-server";
+        version = "2.0.3";
+        src = ./language-server;
+        buildInputs = [
+          coq_8_19
+          dune_3
+        ] ++ (with coq.ocamlPackages; [
+          lablgtk3-sourceview3
+          glib
+          gnome.adwaita-icon-theme
+          wrapGAppsHook
+          ocaml
+          yojson
+          zarith
+          findlib
+          ppx_inline_test
+          ppx_assert
+          ppx_sexp_conv
+          ppx_deriving
+          ppx_optcomp
+          ppx_import
+          sexplib
+          ppx_yojson_conv
+          lsp
+          sel
+        ]);
+      };
+
+    packages.vscoq-language-server-coq-master =
       # Notice the reference to nixpkgs here.
       with import nixpkgs { inherit system; };
       let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in
@@ -68,18 +140,32 @@
         buildInputs = self.packages.${system}.vscoq-client.buildInputs;
       };
 
-    devShells.vscoq-language-server = 
+    devShells.vscoq-language-server-coq-8-18 = 
+        with import nixpkgs { inherit system; };
+        mkShell {
+            buildInputs =
+            self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs;
+        };
+        
+    devShells.vscoq-language-server-8-19 = 
+      with import nixpkgs { inherit system; };
+      mkShell {
+        buildInputs =
+          self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs;
+      };
+    
+    devShells.vscoq-language-server-coq-master = 
       with import nixpkgs { inherit system; };
       mkShell {
         buildInputs =
-          self.packages.${system}.vscoq-language-server.buildInputs;
+          self.packages.${system}.vscoq-language-server-coq-master.buildInputs;
       };
 
     devShells.default = 
       with import nixpkgs { inherit system; };
       mkShell {
         buildInputs =
-          self.packages.${system}.vscoq-language-server.buildInputs
+          self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs
           ++ (with ocamlPackages; [
             ocaml-lsp
           ]);

From 87dd6d0e1de6afb027558851f8dd58eb540e7422 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Mon, 5 Feb 2024 17:41:59 +0100
Subject: [PATCH 28/31] Fix typo in flake

---
 flake.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/flake.nix b/flake.nix
index 21c90383b..f4652bf89 100644
--- a/flake.nix
+++ b/flake.nix
@@ -147,7 +147,7 @@
             self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs;
         };
         
-    devShells.vscoq-language-server-8-19 = 
+    devShells.vscoq-language-server-coq-8-19 = 
       with import nixpkgs { inherit system; };
       mkShell {
         buildInputs =

From bf063d8c4e800b423ce0d274c0bdd95bab45705b Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Tue, 6 Feb 2024 11:46:14 +0100
Subject: [PATCH 29/31] Fix flake + adapt to
 https://github.com/coq/coq/pull/18529

Fixing Coq pin in flake and adding correction to make coq master
branch compile.
---
 flake.lock                      | 8 ++++----
 flake.nix                       | 8 ++++++--
 language-server/dm/parTactic.ml | 4 ++++
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/flake.lock b/flake.lock
index 3f6eb2ac5..e25910e35 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,17 +8,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1692621436,
-        "narHash": "sha256-fLkFHuL8vu4v7Oc9v2701d7pVM/eS/7mCJTEuAFfksA=",
+        "lastModified": 1707209540,
+        "narHash": "sha256-C3ZnIXZQptLo76iqltf/GYu/EqFU5yT7nSMClKTriiI=",
         "owner": "coq",
         "repo": "coq",
-        "rev": "fbaea89860348ca2b2ca485e52df7215bea27746",
+        "rev": "b157d65080076498ad04dd3918c1e508eb9740c0",
         "type": "github"
       },
       "original": {
         "owner": "coq",
         "repo": "coq",
-        "rev": "fbaea89860348ca2b2ca485e52df7215bea27746",
+        "rev": "b157d65080076498ad04dd3918c1e508eb9740c0",
         "type": "github"
       }
     },
diff --git a/flake.nix b/flake.nix
index f4652bf89..89bcc24eb 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,7 +5,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    coq-master = { url = "github:coq/coq/fbaea89860348ca2b2ca485e52df7215bea27746"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master = { url = "github:coq/coq/b157d65080076498ad04dd3918c1e508eb9740c0"; }; # Should be kept in sync with PIN_COQ in CI workflow
     coq-master.inputs.nixpkgs.follows = "nixpkgs";
 
   };
@@ -156,9 +156,13 @@
     
     devShells.vscoq-language-server-coq-master = 
       with import nixpkgs { inherit system; };
+      let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in
       mkShell {
         buildInputs =
-          self.packages.${system}.vscoq-language-server-coq-master.buildInputs;
+          self.packages.${system}.vscoq-language-server-coq-master.buildInputs
+          ++ (with ocamlPackages; [
+            ocaml-lsp
+          ]);
       };
 
     devShells.default = 
diff --git a/language-server/dm/parTactic.ml b/language-server/dm/parTactic.ml
index 4f85bace2..169e62bc7 100644
--- a/language-server/dm/parTactic.ml
+++ b/language-server/dm/parTactic.ml
@@ -60,7 +60,11 @@ let assign_tac ~abstract res : unit Proofview.tactic =
       tclUNIT ()
   end)
 
+[%%if coq = "8.18" || coq = "8.19"]
 let command_focus = Proof.new_focus_kind ()
+[%%else]
+let command_focus = Proof.new_focus_kind "vscoq_command_focus"
+[%%endif]
 
 let worker_solve_one_goal { TacticJob.state; ast; goalno; goal } ~send_back =
   let focus_cond = Proof.no_cond command_focus in

From cd0d7670bcb22bfbeaf1a3909f471916ae7742b0 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Tue, 6 Feb 2024 17:02:56 +0100
Subject: [PATCH 30/31] Update .github/workflows/ci.yml

Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 396c2dfd8..066492f3a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -57,7 +57,7 @@ jobs:
       matrix:
         os: [ubuntu-latest]
         ocaml-compiler: [4.13.x]
-        coq: [8.18.0, 8.19+rc1]
+        coq: [8.18.0, 8.19+rc1, dev]
     runs-on: ${{ matrix.os }}
     steps:
     - name: Checkout

From bf48804e9e829ba6be06dd8e995d8a04df4b6fad Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 6 Feb 2024 23:43:14 +0100
Subject: [PATCH 31/31] Update .github/workflows/ci.yml

---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 066492f3a..9f33d8b15 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -73,7 +73,7 @@ jobs:
         OPAMYES: true
       run: |
         opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-        opam pin add coq-core ${{ matrix.coq }}
+        opam install coq-core.${{ matrix.coq }}
         opam pin add vscoq-language-server ./language-server/ --with-doc --with-test -y
 
     - run: |