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.

1 files changed, 11 insertions, 7 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 620efbafd6..1336e3e8bf 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -202,17 +202,21 @@ let lift_univs cb subst auctx0 =
     let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
     subst, (Polymorphic auctx)
 
-let cook_constr { Opaqueproof.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
-  (* For now the STM only handles deferred computation of monomorphic
-    constants. The API will need to be adapted when it's not the case
-    anymore. *)
-  let () = assert (AUContext.is_empty abs_ctx) in
+  let ainst = Instance.of_array (Array.init univs Level.var) in
+  let usubst = Instance.append usubst ainst in
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps in
-  abstract_constant_body (expmod c) hyps
+  let c = abstract_constant_body (expmod c) hyps in
+  univs + AUContext.size abs_ctx, c
+
+let cook_constr infos univs c =
+  let fold info (univs, c) = cook_constr info (univs, c) in
+  let (_, c) = List.fold_right fold infos (univs, c) in
+  c
 
 let cook_constant { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
@@ -227,7 +231,7 @@ let cook_constant { from = cb; info } =
   | Undef _ as x -> x
   | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
   | OpaqueDef o ->
-    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o)
+    OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
   let const_hyps =