From aba0bc6df25ca6c5a2846bab32eaeb42373d2629 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Tue, 18 Jun 2024 15:14:02 +0200
Subject: [PATCH] Fixing optcomp flags

---
 language-server/dm/documentManager.ml  | 15 ++++++++-------
 language-server/dm/executionManager.ml |  8 ++++----
 2 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index bcd5186a1..a5697460e 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -383,22 +383,23 @@ let get_completions st pos =
     | None -> Error ("Can't get completions")
     | Some lemmas -> Ok (lemmas)
 
-[%%if coq = "8.20"]
+[%%if coq = "8.18" || coq = "8.19"]
 let parse_entry st pos entry pattern =
   let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string pattern) in
   let st = match Document.find_sentence_before st.document pos with
-  | None -> Vernacstate.(Synterp.parsing st.init_vs.synterp)
-  | Some { synterp_state } -> Vernacstate.Synterp.parsing synterp_state
+  | None -> st.init_vs.Vernacstate.synterp.parsing
+  | Some { synterp_state } -> synterp_state.Vernacstate.Synterp.parsing
   in
   Vernacstate.Parser.parse st entry pa
 [%%else]
 let parse_entry st pos entry pattern =
   let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string pattern) in
   let st = match Document.find_sentence_before st.document pos with
-  | None -> st.init_vs.Vernacstate.synterp.parsing
-  | Some { synterp_state } -> synterp_state.Vernacstate.Synterp.parsing
-  in
-  Vernacstate.Parser.parse st entry pa
+  | None -> Vernacstate.(Synterp.parsing st.init_vs.synterp)
+  | Some { synterp_state } -> Vernacstate.Synterp.parsing synterp_state
+  in  
+  Pcoq.unfreeze st;
+  Pcoq.Entry.parse entry pa
 [%%endif]
 
 let about st pos ~pattern =
diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 8e28c13c9..6504f0610 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -204,10 +204,7 @@ let definition_using e s ~fixnames:_ ~using ~terms =
 let definition_using = Proof_using.definition_using
 [%%endif]
 
-[%%if coq = "8.20"]
-let add_using proof proof_using _ =
-  Declare.Proof.set_proof_using proof proof_using |> snd
-[%%else]
+[%%if coq = "8.18" || coq = "8.19"]
 let add_using proof proof_using lemmas =
       let env = Global.env () in
       let sigma, _ = Declare.Proof.get_current_context proof in
@@ -223,6 +220,9 @@ let add_using proof proof_using lemmas =
         using;
       let _, pstate = Declare.Proof.set_used_variables proof ~using in
       pstate
+[%%else]
+let add_using proof proof_using _ =
+  Declare.Proof.set_proof_using proof proof_using |> snd
 [%%endif]
 
 let interp_qed_delayed ~proof_using ~state_id ~st =