From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:09:30 +0200
Subject: [declare] Move proof information to declare.

At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
---
 plugins/funind/functional_principles_proofs.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 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 b864b18887..652f942cb9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -856,9 +856,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let lemma =
     Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type
   in
-  let lemma, _ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
+  let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
-    Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+    Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
+      ~idopt:None
   in
   evd
 
-- 
cgit v1.2.3