Fixing optcomp flags

coq · Jun 18, 2024 · aba0bc6 · aba0bc6
1 parent fa77f04
commit aba0bc6
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 11 deletions.
diff --git 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
@@ -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 =