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

(limited to 'checker/mod_checking.mli')

diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index dbc81c8507..7aa1f837a0 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -8,6 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit
+val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit
 
 val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
-- 
cgit v1.2.3