[api] [coq] fixup for merge from main

ejgallego · Feb 22, 2023 · 29d4cf9 · 29d4cf9
1 parent 383ce41
commit 29d4cf9
Showing 1 changed file with 5 additions and 2 deletions.
diff --git 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 "