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, 5 insertions, 3 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0ecfbacb09..d305a58ccc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -416,8 +416,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
       ComDefinition.do_definition
         ~program_mode:false
-        fname
-        Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl
+        ~name:fname
+        ~poly:false
+        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+        ~kind:Decl_kinds.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
          List.fold_left
@@ -434,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl;
+       ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->