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.

4 files changed, 37 insertions, 12 deletions

diff --git a/checker/check.ml b/checker/check.ml
index c5bc59e72a..747d7c43a1 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -51,7 +51,7 @@ let pr_path sp =
 type compilation_unit_name = DirPath.t
 
 type seg_univ = Univ.ContextSet.t * bool
-type seg_proofs = Constr.constr option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr) option array
 
 type library_t = {
   library_name : compilation_unit_name;
@@ -98,9 +98,18 @@ let access_opaque_table dp i =
     with Not_found -> assert false
   in
   assert (i < Array.length t);
-  t.(i)
+  match t.(i) with
+  | None -> None
+  | Some (info, n, c) -> Some (Cooking.cook_constr info n c)
 
-let () = Mod_checking.set_indirect_accessor access_opaque_table
+let access_discharge = Cooking.cook_constr
+
+let indirect_accessor = {
+  Opaqueproof.access_proof = access_opaque_table;
+  Opaqueproof.access_discharge = access_discharge;
+}
+
+let () = Mod_checking.set_indirect_accessor indirect_accessor
 
 let check_one_lib admit senv (dir,m) =
   let md = m.library_compiled in
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
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
diff --git a/checker/values.ml b/checker/values.ml
index 031f05dd6b..6dbf281f49 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -131,7 +131,7 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
 let rec v_constr =
   Sum ("constr",0,[|
     [|Int|]; (* Rel *)
-    [|Fail "Var"|]; (* Var *)
+    [|v_id|]; (* Var *)
     [|Fail "Meta"|]; (* Meta *)
     [|Fail "Evar"|]; (* Evar *)
     [|v_sort|]; (* Sort *)
@@ -383,6 +383,22 @@ let v_libsum =
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
 
-let v_opaques = Array (Opt v_constr)
+let v_ndecl = v_sum "named_declaration" 0
+    [| [|v_binder_annot v_id; v_constr|];               (* LocalAssum *)
+       [|v_binder_annot v_id; v_constr; v_constr|] |]   (* LocalDef *)
+
+let v_nctxt = List v_ndecl
+
+let v_work_list =
+  let v_abstr = v_pair v_instance (Array v_id) in
+  Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|])
+
+let v_abstract =
+  Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |])
+
+let v_cooking_info =
+  Tuple ("cooking_info", [|v_work_list; v_abstract|])
+
+let v_opaques = Array (Opt (Tuple ("opaque", [| List v_cooking_info; Int; v_constr |])))
 let v_univopaques =
   Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))