From 3ef2bd35926a83fbcfd34d03e1fb1db894a39627 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 8 Jul 2020 14:06:19 +0200
Subject: declare: Add [save_regular] API for obligation-ignoring proofs

---
 plugins/funind/gen_principle.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'plugins/funind/gen_principle.ml')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 730cf42fe8..45b1713441 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1526,10 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lemma =
             fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
-          let pm = Declare.OblState.empty in
-          let _pm, _ =
-            Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent
-              ~idopt:None
+          let (_ : _ list) =
+            Declare.Proof.save_regular ~proof:lemma
+              ~opaque:Vernacexpr.Transparent ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -1599,10 +1598,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                        (proving_tac i)))
                  lemma)
           in
-          let pm = Declare.OblState.empty in
-          let _pm, _ =
-            Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent
-              ~idopt:None
+          let (_ : _ list) =
+            Declare.Proof.save_regular ~proof:lemma
+              ~opaque:Vernacexpr.Transparent ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
-- 
cgit v1.2.3