From 29d4cf9bc325bc4d8670bed25f6ca5ea34db21df Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 22 Feb 2023 02:44:01 +0100
Subject: [PATCH] [api] [coq] fixup for merge from main

---
 coq/save.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/coq/save.ml b/coq/save.ml
index b240b77c..bf25b69a 100644
--- a/coq/save.ml
+++ b/coq/save.ml
@@ -1,8 +1,11 @@
 (* Taken from sertop / Coq *)
+let get_all_proof_names () =
+  (Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"])
+
 let ensure_no_pending_proofs ~in_file ~st =
   match st.Vernacstate.lemmas with
-  | Some lemmas ->
-    let pfs = Vernacstate.LemmaStack.get_all_proof_names lemmas in
+  | Some _lemmas ->
+    let pfs = get_all_proof_names () in
     CErrors.user_err
       Pp.(
         str "There are pending proofs in file "