Merge PR coq#17792: Stop relying on opaque proof accessors in funind.

Reviewed-by: Matafou Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre · Jul 3, 2023 · c0e7d0c · c0e7d0c
2 parents 9790a21 + cac8662
commit c0e7d0c
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 14 deletions.
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
@@ -829,8 +829,10 @@ let generate_equation_lemma env evd fnames f fun_num nb_params nb_args rec_args_
       , 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 Library.indirect_accessor f_def)
+  let f_body = match f_def.const_body with
+  | Def d -> d
+  | OpaqueDef _ | Primitive _ | Undef _ ->
+    CErrors.user_err (Pp.str "Definition without a body")
   in
   let f_body = EConstr.of_constr f_body in
   let params, f_body_with_params = decompose_lambda_n evd nb_params f_body in
@@ -991,14 +993,15 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
         ; args = List.map fresh_decl princ_info.args }
       in
       let get_body const =
-        match Global.body_of_constant Library.indirect_accessor const with
-        | Some (body, _, _) ->
-          let env = Global.env () in
+        let env = Global.env () in
+        let body = Environ.lookup_constant const env in
+        match body.Declarations.const_body with
+        | Def body ->
           let sigma = Evd.from_env env in
           Tacred.cbv_norm_flags
             (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
             env sigma (EConstr.of_constr body)
-        | None -> user_err Pp.(str "Cannot define a principle over an axiom ")
+        | Undef _ | Primitive _ | OpaqueDef _ -> user_err Pp.(str "Cannot define a principle over an axiom ")
       in
       let fbody = get_body fnames.(fun_num) in
       let f_ctxt, f_body = decompose_lambda sigma fbody in

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
@@ -1218,18 +1218,20 @@ let get_funs_constant mp =
   function
   | const ->
     let find_constant_body const =
-      match Global.body_of_constant Library.indirect_accessor const with
-      | Some (body, _, _) ->
+      let env = Global.env () in
+      let body = Environ.lookup_constant const env in
+      match body.Declarations.const_body with
+      | Def body ->
         let body =
           Tacred.cbv_norm_flags
             (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-            (Global.env ())
-            (Evd.from_env (Global.env ()))
+            env
+            (Evd.from_env env)
             (EConstr.of_constr body)
         in
         let body = EConstr.Unsafe.to_constr body in
         body
-      | None ->
+      | Undef _ | OpaqueDef _ | Primitive _ ->
         CErrors.user_err Pp.(str "Cannot define a principle over an axiom ")
     in
     let f = find_constant_body const in
@@ -2057,9 +2059,9 @@ let make_graph (f_ref : GlobRef.t) =
             ++ Termops.pr_global_env env (ConstRef c))
     | _ -> CErrors.user_err Pp.(str "Not a function reference")
   in
-  match Global.body_of_constant_body Library.indirect_accessor c_body with
-  | None -> CErrors.user_err (Pp.str "Cannot build a graph over an axiom!")
-  | Some (body, _, _) ->
+  match c_body.Declarations.const_body with
+  | Undef _ | Primitive _ | OpaqueDef _ -> CErrors.user_err (Pp.str "Cannot build a graph over an axiom!")
+  | Def body ->
     let env = Global.env () in
     let extern_body, extern_type =
       with_full_print