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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction')

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