Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

1 files changed, 9 insertions, 4 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ce3b5a82d6..a904b81d81 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -990,14 +990,19 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       ]
   in
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
+  let info = Lemmas.Info.make
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+
   let lemma = Lemmas.start_lemma
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
-    (mk_equation_id f_id)
-    Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
-    evd
-  lemma_type
+      ~name:(mk_equation_id f_id)
+      ~poly:false
+      ~info
+      evd
+      lemma_type
   in
   let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
   let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in