Adapt to PR #18795

src/eqdec.ml

@@ -157,7 +157,7 @@ let derive_eq_dec ~pm env sigma ~poly ind =
      let cinfo = Declare.CInfo.make ~name:id ~typ:(to_constr !evdref stmt) () in
      let info = Declare.Info.make ~poly ~hook () in
      let pm = Declare.Obls.add_definition ~pm ~cinfo ~info
-              ~uctx:(Evd.evar_universe_context !evdref)
+              ~uctx:(Evd.evar_universe_context !evdref) ~opaque:false
               ~tactic:(eqdec_tac ()) [||]
      in fst pm)
     pm indsl

src/equations.ml

@@ -94,7 +94,7 @@ let define_unfolding_eq ~pm env evd flags p unfp prog prog' ei hook =
         ~kind:(Decls.IsDefinition info.decl_kind)
         ()
     in
-    let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~tactic:tac ~uctx [||] in
+    let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~tactic:tac ~uctx ~opaque:false [||] in
     pm
   in
   let pm = List.fold_left fold pm subproofs in
@@ -112,7 +112,7 @@ let define_unfolding_eq ~pm env evd flags p unfp prog prog' ei hook =
   let obl_hook = Declare.Hook.make_g hook_eqs in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~cinfo ~info ~reduce:(fun x -> x)
-      ~tactic:tac ~obl_hook
+      ~tactic:tac ~obl_hook ~opaque:false
       ~uctx:(Evd.evar_universe_context evd) [||]
   in pm
 

src/noconf_hom.ml

@@ -102,8 +102,8 @@ let derive_noConfusion_package ~pm env sigma ~poly (ind,u as indu) indid ~prefix
   let oblinfo, _, term, ty = RetrieveObl.retrieve_obligations env noid sigma 0 term ty in
   let cinfo = Declare.CInfo.make ~name:packid ~typ:ty () in
   let info = Declare.Info.make ~hook ~poly ~scope ~kind () in
-  let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info
-             ~term ~tactic ~uctx:(Evd.evar_universe_context sigma) oblinfo in
+  let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~opaque:false
+             ~body:term ~tactic ~uctx:(Evd.evar_universe_context sigma) oblinfo in
   pm
 
 let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =

src/principles.ml

@@ -1286,7 +1286,7 @@ let declare_funelim ~pm info env evd is_rec protos progs
   let newty = collapse_term_qualities (Evd.evar_universe_context !evd) (EConstr.to_constr !evd newty) in 
   let cinfo = Declare.CInfo.make ~name:(Nameops.add_suffix id "_elim") ~typ:newty () in
   let info = Declare.Info.make ~poly:info.poly ~scope:info.scope ~hook:(Declare.Hook.make hookelim) ~kind:(Decls.IsDefinition info.decl_kind) () in
-  let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~tactic
+  let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~tactic ~opaque:false
       ~uctx:(Evd.evar_universe_context !evd) [||] in
   pm
 
@@ -1401,7 +1401,7 @@ let declare_funind ~pm info alias env evd is_rec protos progs
           ~kind:(Decls.IsDefinition info.term_info.decl_kind)
           () in
       let obl_hook = Declare.Hook.make_g hookind in
-      Declare.Obls.add_definition ~pm ~cinfo ~info ~obl_hook
+      Declare.Obls.add_definition ~pm ~cinfo ~info ~obl_hook ~opaque:false
         ~tactic:(Tacticals.tclTRY tactic) ~uctx [||]
     in
     match res with
@@ -1802,7 +1802,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
       let cinfo = Declare.CInfo.make ~name:ideq ~typ:c () in
       let info = Declare.Info.make ~kind:(Decls.IsDefinition info.decl_kind) ~poly () in
       let obl_hook = Declare.Hook.make_g hook in
-      let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~obl_hook
+      let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~obl_hook ~opaque:false
                ~tactic:tac ~uctx:(Evd.evar_universe_context !evd) [||] in
       pm
     in List.fold_left proof pm stmts

src/splitting.ml

@@ -1205,7 +1205,7 @@ let solve_equations_obligations_program ~pm flags recids loc i sigma hook =
   let info = Declare.Info.make ~poly ~scope ~kind () in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~cinfo ~info 
-      ~obl_hook ~term ~uctx:(Evd.evar_universe_context sigma)
+      ~obl_hook ~body:term ~uctx:(Evd.evar_universe_context sigma)
       ~reduce ~opaque:false oblsinfo in
   pm
 

src/subterm.ml

@@ -265,7 +265,7 @@ let derive_subterm ~pm env sigma ~poly (ind, u as indu) =
     let cinfo = Declare.CInfo.make ~name:id ~typ () in
     let info = Declare.Info.make ~poly ~scope:Locality.(Global ImportDefaultBehavior)
         ~kind:Decls.(IsDefinition Instance) ~hook:(Declare.Hook.make hook) () in
-    let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~term:constr ~uctx
+    let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~body:constr ~uctx ~opaque:false
                                 ~tactic:(solve_subterm_tac ()) obls in
     pm
   in