From e7ffa1bfa25300a25c1e81583b77d2d7587bbb5d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 May 2019 14:27:36 +0200
Subject: Do not substitute opaque constants when discharging.

Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.
---
 checker/mod_checking.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ccce0bd9a7..0684623a81 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,13 +8,13 @@ open Environ
 
 (** {6 Checking constants } *)
 
-let get_proof = ref (fun _ _ -> assert false)
-let set_indirect_accessor f = get_proof := f
-
-let indirect_accessor = {
-  Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
+let indirect_accessor = ref {
+  Opaqueproof.access_proof = (fun _ _ -> assert false);
+  Opaqueproof.access_discharge = (fun _ _ _ -> assert false);
 }
 
+let set_indirect_accessor f = indirect_accessor := f
+
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   (* Locally set the oracle for further typechecking *)
@@ -40,7 +40,7 @@ let check_constant_declaration env kn cb =
   let body = match cb.const_body with
   | Undef _ | Primitive _ -> None
   | Def c -> Some (Mod_subst.force_constr c)
-  | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o)
+  | OpaqueDef o -> Some (Opaqueproof.force_proof !indirect_accessor otab o)
   in
   let () =
     match body with
-- 
cgit v1.2.3