Merge PR #10201: Remove access to indirect opaques in the kernel

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

4 files changed, 5 insertions, 5 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 9db7c8d8d3..051d1f8e0f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -115,7 +115,7 @@ let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr)
 
 let get_opaque env c =
   EConstr.of_constr
-    (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+    (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c)
 
 let applistc c args = EConstr.mkApp (c, Array.of_list args)
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index cffe8a3e78..f2b9ba2ec6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -951,7 +951,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
   let f_def = Global.lookup_constant (fst (destConst evd f)) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
-  let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in
+  let (f_body, _) = Option.get (Global.body_of_constant_body Library.indirect_accessor f_def) in
   let f_body = EConstr.of_constr f_body in
   let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
   let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1082,7 +1082,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
       }
     in
     let get_body const =
-      match Global.body_of_constant const with
+      match Global.body_of_constant Library.indirect_accessor const with
 	| Some (body, _) ->
           let env = Global.env () in
           let sigma = Evd.from_env env in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f51c6dc6be..2c107d39d9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -413,7 +413,7 @@ let get_funs_constant mp =
   in
   function const ->
     let find_constant_body const =
-      match Global.body_of_constant const with
+      match Global.body_of_constant Library.indirect_accessor const with
 	| Some (body, _) ->
 	    let body = Tacred.cbv_norm_flags
 	      (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ce7d149ae1..a6b088de0c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -851,7 +851,7 @@ let make_graph ~pstate (f_ref : GlobRef.t) =
       end
     | _ -> raise (UserError (None, str "Not a function reference") )
   in
-  (match Global.body_of_constant_body c_body with
+  (match Global.body_of_constant_body Library.indirect_accessor c_body with
      | None -> error "Cannot build a graph over an axiom!"
      | Some (body, _) ->
        let env = Global.env () in