From d3c931cd8c84d1b7d9d5763e20221d51700f0709 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 May 2019 19:22:30 +0200
Subject: Remove the indirect opaque accessor hooks from Opaqueproof.

We simply pass them as arguments, now that they are not called by the
kernel anymore.

The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
---
 plugins/extraction/extraction.ml               | 2 +-
 plugins/funind/functional_principles_proofs.ml | 4 ++--
 plugins/funind/functional_principles_types.ml  | 2 +-
 plugins/funind/indfun.ml                       | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3