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/functional_principles_proofs.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b743329e7d..743afe4177 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -863,9 +863,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let lemma, _ =
     Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
   in
-  let pm = Declare.OblState.empty in
-  let _pm, _ =
-    Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent
+  let (_ : _ list) =
+    Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
       ~idopt:None
   in
   evd
-- 
cgit v1.2.3