From bedfe0c65df429da61f589e9a11a85b1f2ca5cbd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Fri, 31 Jan 2025 10:32:12 +0100
Subject: [PATCH 1/2] Adapt w.r.t coq/coq#20167.

---
 language-server/dm/document.ml | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
index 51311d96..587a831d 100644
--- a/language-server/dm/document.ml
+++ b/language-server/dm/document.ml
@@ -419,7 +419,19 @@ type diff =
   | Added of pre_sentence list
   | Equal of (sentence_id * pre_sentence) list
 
-
+let tok_equal t1 t2 =
+  let open Tok in
+  match t1, t2 with
+  | KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
+  | IDENT s1, IDENT s2 -> CString.equal s1 s2
+  | FIELD s1, FIELD s2 -> CString.equal s1 s2
+  | NUMBER n1, NUMBER n2 -> NumTok.Unsigned.equal n1 n2
+  | STRING s1, STRING s2 -> CString.equal s1 s2
+  | LEFTQMARK, LEFTQMARK -> true
+  | BULLET s1, BULLET s2 -> CString.equal s1 s2
+  | EOI, EOI -> true
+  | QUOTATION(s1,t1), QUOTATION(s2,t2) -> CString.equal s1 s2 && CString.equal t1 t2
+  | _ -> false
 
 let same_tokens (s1 : sentence) (s2 : pre_sentence) =
   match s1.ast, s2.ast with
@@ -460,9 +472,10 @@ let string_of_diff doc l =
 
 let rec stream_tok n_tok acc str begin_line begin_char =
   let e = LStream.next (get_keyword_state ()) str in
-  if Tok.(equal e EOI) then
+  match e with
+  | Tok.EOI ->
     List.rev acc
-  else
+  | _ ->
     stream_tok (n_tok+1) (e::acc) str begin_line begin_char
     (*
 let parse_one_sentence stream ~st =

From cae233fbd0b117f7d356c6f7867c1e018af42841 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Fri, 31 Jan 2025 15:14:37 +0100
Subject: [PATCH 2/2] fix: update flake

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

diff --git a/flake.nix b/flake.nix
index 6953a54d..fd5ae433 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
 
-    coq-master = { url = "github:coq/coq/d6dd8a618cbf628a6580c9a42db0cf5f44606bea"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master = { url = "github:coq/coq/3e7c26f8bb991e7335162647017edf21b2afd974"; }; # Should be kept in sync with PIN_COQ in CI workflow
     coq-master.inputs.nixpkgs.follows = "nixpkgs";
 
   };