Lazyconstr -> Opaqueproof

Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.

33 files changed, 232 insertions, 252 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index aedd09560..6415a1a78 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -58,7 +58,7 @@ Copcodes
 Cemitcodes
 Nativevalues
 Future
-Lazyconstr
+Opaqueproof
 Declareops
 Retroknowledge
 Conv_oracle
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 82155a305..eefd07e60 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -58,7 +58,7 @@ let ppevar evk = pp (str (Evd.string_of_existential evk))
 let ppconstr x = pp (Termops.print_constr x)
 let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
 let ppterm = ppconstr
-let ppsconstr x = ppconstr (Lazyconstr.force x)
+let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index af6992252..58465849c 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -719,7 +719,7 @@ let compile env c =
 let compile_constant_body env = function
   | Undef _ | OpaqueDef _ -> BCconstant
   | Def sb ->
-      let body = Lazyconstr.force sb in
+      let body = Mod_subst.force_constr sb in
       match kind_of_term body with
 	| Const kn' ->
 	    (* we use the canonical name of the constant*)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 75642648d..f81bcceb3 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -109,7 +109,7 @@ let abstract_constant_type =
 let abstract_constant_body =
   List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
 
-type recipe = { from : constant_body; info : Lazyconstr.cooking_info }
+type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
 type result =
@@ -118,21 +118,22 @@ type result =
 
 let on_body ml hy f = function
   | Undef _ as x -> x
-  | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
-  | OpaqueDef lc ->
-    OpaqueDef (Lazyconstr.discharge_direct_lazy_constr ml hy f lc)
+  | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs)))
+  | OpaqueDef o ->
+    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
+                 { Opaqueproof.modlist = ml; abstract = hy } o)
 
 let constr_of_def = function
   | Undef _ -> assert false
-  | Def cs -> Lazyconstr.force cs
-  | OpaqueDef lc -> Lazyconstr.force_opaque lc
+  | Def cs -> Mod_subst.force_constr cs
+  | OpaqueDef lc -> Opaqueproof.force_proof lc
 
-let cook_constr { Lazyconstr.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract } c =
   let cache = Hashtbl.create 13 in
   let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
   abstract_constant_body (expmod_constr cache modlist c) hyps
 
-let cook_constant env { from = cb; info = { Lazyconstr.modlist; abstract } } =
+let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
   let cache = Hashtbl.create 13 in
   let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
   let body = on_body modlist hyps
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 05c7a2040..8493b81d8 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -14,7 +14,7 @@ open Univ
 
 (** {6 Cooking the constants. } *)
 
-type recipe = { from : constant_body; info : Lazyconstr.cooking_info }
+type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 
 type inline = bool
 
@@ -23,9 +23,9 @@ type result =
     * Context.section_context option
 
 val cook_constant : env -> recipe -> result
-val cook_constr : Lazyconstr.cooking_info -> Term.constr -> Term.constr
+val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
 
 (** {6 Utility functions used in module [Discharge]. } *)
 
-val expmod_constr : Lazyconstr.work_list -> constr -> constr
+val expmod_constr : Opaqueproof.work_list -> constr -> constr
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ef56ae512..e6025790a 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -37,8 +37,8 @@ type inline = int option
 
 type constant_def =
   | Undef of inline
-  | Def of Lazyconstr.constr_substituted
-  | OpaqueDef of Lazyconstr.lazy_constr
+  | Def of constr Mod_subst.substituted
+  | OpaqueDef of Opaqueproof.opaque
 
 (* some contraints are in constant_constraints, some other may be in
  * the OpaueDef *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 21a961fc3..7c852a755 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -8,7 +8,6 @@
 
 open Declarations
 open Mod_subst
-open Lazyconstr
 open Util
 
 (** Operations concernings types in [Declarations] :
@@ -18,14 +17,14 @@ open Util
 
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
-  | Def c -> Some (Lazyconstr.force c)
-  | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc)
+  | Def c -> Some (force_constr c)
+  | OpaqueDef o -> Some (Opaqueproof.force_proof o)
 
 let constraints_of_constant cb = Univ.union_constraints cb.const_constraints
  (match cb.const_body with
   | Undef _ -> Univ.empty_constraint
   | Def c -> Univ.empty_constraint
-  | OpaqueDef lc -> snd (Lazyconstr.force_opaque_w_constraints lc))
+  | OpaqueDef o -> Opaqueproof.force_constraints o)
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
@@ -57,8 +56,8 @@ let subst_const_type sub arity = match arity with
 
 let subst_const_def sub def = match def with
   | Undef _ -> def
-  | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+  | Def c -> Def (subst_constr sub c)
+  | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
 
 let subst_const_body sub cb =
   assert (List.is_empty cb.const_hyps); (* we're outside sections *)
@@ -104,7 +103,7 @@ let hcons_const_type = function
 let hcons_const_def = function
   | Undef inl -> Undef inl
   | Def l_constr ->
-    let constr = force l_constr in
+    let constr = force_constr l_constr in
     Def (from_val (Term.hcons_constr constr))
   | OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
 
@@ -238,7 +237,7 @@ let hcons_mind mib =
 
 let join_constant_body cb =
   match cb.const_body with
-  | OpaqueDef d -> Lazyconstr.join_lazy_constr d
+  | OpaqueDef o -> Opaqueproof.join_opaque o
   | _ -> ()
 
 let string_of_side_effect = function
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 93677e5a9..15db39328 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -189,7 +189,7 @@ exception NotEvaluableConst of const_evaluation_result
 let constant_value env kn =
   let cb = lookup_constant kn env in
   match cb.const_body with
-    | Def l_body -> Lazyconstr.force l_body
+    | Def l_body -> Mod_subst.force_constr l_body
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 7d318add5..bcd366f1a 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -12,7 +12,7 @@ Cbytecodes
 Copcodes
 Cemitcodes
 Nativevalues
-Lazyconstr
+Opaqueproof
 Declareops
 Retroknowledge
 Conv_oracle
diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml
deleted file mode 100644
index 23d6d559d..000000000
--- a/kernel/lazyconstr.ml
+++ /dev/null
@@ -1,134 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Mod_subst
-
-type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
-type cooking_info = { modlist : work_list; abstract : Context.named_context } 
-
-(** [constr_substituted] are [constr] with possibly pending
-    substitutions of kernel names. *)
-
-type constr_substituted = constr substituted
-
-let from_val = from_val
-
-let force = force subst_mps
-
-let subst_constr_subst = subst_substituted
-
-(** Opaque proof terms might be in some external tables.
-    The [force_opaque] function below allows to access these tables,
-    this might trigger the read of some extra parts of .vo files.
-    In the [Indirect] case, we accumulate "manually" a substitution
-    list, the younger one coming first. Nota: no [Direct] constructor
-    should end in a .vo, this is checked by coqchk.
-*)
-
-type proofterm = (constr * Univ.constraints) Future.computation
-type lazy_constr =
-  (* subst, lib, index *)
-  | Indirect of substitution list * DirPath.t * int
-  (* opaque in section or interactive session *)
-  | Direct of cooking_info list * (constr_substituted * Univ.constraints) Future.computation
-
-(* TODO : this hcons function could probably be improved (for instance
-   hash the dir_path in the Indirect case) *)
-
-let subst_lazy_constr sub = function
-  | Direct ([],cu) ->
-      Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
-        subst_constr_subst sub c, u))
-  | Direct _ -> Errors.anomaly (Pp.str"still direct but not discharged")
-  | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
-
-let iter_direct_lazy_constr f = function
-  | Indirect _ -> Errors.anomaly (Pp.str "iter_direct_lazy_constr")
-  | Direct (d,cu) ->
-      Direct (d, Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> f (force c); c, u))
-
-let discharge_direct_lazy_constr modlist abstract  f = function
-  | Indirect _ -> Errors.anomaly (Pp.str "discharge_direct_lazy_constr")
-  | Direct (d,cu) ->
-      Direct ({ modlist; abstract }::d,
-        Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
-          from_val (f (force c)), u))
-
-let default_get_opaque dp _ =
-  Errors.error
-    ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
-let default_get_univ dp _ =
-  Errors.error
-    ("Cannot access universe constraints of opaque proofs in library " ^
-    DirPath.to_string dp)
-
-let default_mk_indirect _ = None
-
-let default_join_indirect_local_opaque _ _ = ()
-let default_join_indirect_local_univ _ _ = ()
-
-let get_opaque = ref default_get_opaque
-let get_univ = ref default_get_univ
-let join_indirect_local_opaque = ref default_join_indirect_local_opaque
-let join_indirect_local_univ = ref default_join_indirect_local_univ
-
-let mk_indirect = ref default_mk_indirect
-let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_univ_accessor f = (get_univ := f)
-let set_indirect_creator f = (mk_indirect := f)
-let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
-let set_join_indirect_local_univ f = join_indirect_local_univ := f
-
-let reset_indirect_creator () = mk_indirect := default_mk_indirect
-
-let force_lazy_constr = function
-  | Direct (_,c) -> Future.force c
-  | Indirect (l,dp,i) ->
-      let c = Future.force (!get_opaque dp i) in
-      List.fold_right subst_constr_subst l (from_val c),
-      Future.force
-        (Option.default
-          (Future.from_val Univ.empty_constraint)
-          (!get_univ dp i))
-
-let join_lazy_constr = function
-  | Direct (_,c) -> ignore(Future.force c)
-  | Indirect (_,dp,i) ->
-      !join_indirect_local_opaque dp i;
-      !join_indirect_local_univ dp i
-
-let turn_indirect lc = match lc with
-  | Indirect _ ->
-    Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
-  | Direct (d,cu) ->
-    let cu = Future.chain ~greedy:true ~pure:true cu (fun (c,u) ->
-      (* this constr_substituted shouldn't have been substituted yet *)
-      assert (fst (Mod_subst.repr_substituted c) == None);
-      hcons_constr (force c),u) in
-    match !mk_indirect (d,cu) with
-      | None -> lc
-      | Some (dp,i) -> Indirect ([],dp,i)
-
-let force_opaque lc =
-  let c, _u = force_lazy_constr lc in force c
-let force_opaque_w_constraints lc =
-  let c, u = force_lazy_constr lc in force c, u
-let get_opaque_future_constraints lc = match lc with
-  | Indirect (_,dp,i) -> !get_univ dp i
-  | Direct (_,cu) -> Some(snd (Future.split2 ~greedy:true cu))
-let get_opaque_futures lc = match lc with
-  | Indirect _ -> assert false
-  | Direct (_,cu) ->
-      let cu =
-        Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> force c, u) in
-      Future.split2 ~greedy:true cu
-
-let opaque_from_val cu =
-  Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> from_val c, u))
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 009bcb770..f0d1aca4d 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -546,6 +546,9 @@ let force fsubst r = match r.subst_subst with
 
 let subst_substituted s r = { r with subst_subst = s :: r.subst_subst; }
 
+let force_constr = force subst_mps
+let subst_constr = subst_substituted
+
 (* debug *)
 let repr_substituted r = match r.subst_subst with
 | [] -> None, r.subst_value
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index ddc05380a..34f10b31a 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -152,3 +152,7 @@ val occur_mbid : MBId.t -> substitution -> bool
     - [Some s, a] when r is a delayed substitution [s] applied to [a] *)
 
 val repr_substituted : 'a substituted -> substitution list option * 'a
+
+val force_constr : Term.constr substituted -> Term.constr
+val subst_constr :
+  substitution -> Term.constr substituted -> Term.constr substituted
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 6e656fad9..6c0f1b060 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -80,11 +80,11 @@ let rec check_with_def env struc (idl,c) mp equiv =
 	  let cst = cb.const_constraints +++ cst1 +++ cst2 in
 	  j.uj_val, cst
 	| Def cs ->
-	  let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
+	  let cst1 = Reduction.conv env' c (Mod_subst.force_constr cs) in
 	  let cst = cb.const_constraints +++ cst1 in
           c, cst
       in
-      let def = Def (Lazyconstr.from_val c') in
+      let def = Def (Mod_subst.from_val c') in
       let cb' =
 	{ cb with
 	  const_body = def;
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2942412f0..2bd421bb3 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -345,7 +345,7 @@ let strengthen_const mp_from l cb resolver =
     let kn = KerName.make2 mp_from l in
     let con = constant_of_delta_kn resolver kn in
     { cb with
-      const_body = Def (Lazyconstr.from_val (mkConst con));
+      const_body = Def (Mod_subst.from_val (mkConst con));
       const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) }
 
 let rec strengthen_mod mp_from mp_to mb =
@@ -407,7 +407,7 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	  match constant.const_body with
 	    | Undef _ | OpaqueDef _ -> l
 	    | Def body ->
-	      let constr = Lazyconstr.force body in
+	      let constr = Mod_subst.force_constr body in
 	      add_inline_delta_resolver kn (lev, Some constr) l
 	with Not_found ->
 	  error_no_such_label_sub (con_label con)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 7d542c107..99513319b 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1523,7 +1523,7 @@ and compile_named env sigma auxdefs id =
 let compile_constant env sigma prefix ~interactive con body =
   match body with
   | Def t ->
-      let t = Lazyconstr.force t in
+      let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
       let is_lazy = is_lazy t in
       let code = if is_lazy then mk_lazy code else code in
@@ -1628,7 +1628,7 @@ let rec compile_deps env sigma prefix ~interactive init t =
       else
       let comp_stack, (mind_updates, const_updates) = match cb.const_body with
         | Def t ->
-	   compile_deps env sigma prefix ~interactive init (Lazyconstr.force t)
+	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
         | _ -> init
       in
       let code, name =
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 258f03efd..e6a579c5b 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -639,11 +639,11 @@ and lambda_of_app env sigma f args =
       begin match cb.const_body with
       | Def csubst ->
           if cb.const_inline_code then
-            lambda_of_app env sigma (Lazyconstr.force csubst) args
+            lambda_of_app env sigma (Mod_subst.force_constr csubst) args
           else
           let prefix = get_const_prefix !global_env kn in
           let t =
-            if is_lazy (Lazyconstr.force csubst) then
+            if is_lazy (Mod_subst.force_constr csubst) then
               mkLapp Lforce [|Lconst (prefix, kn)|]
             else Lconst (prefix, kn)
           in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
new file mode 100644
index 000000000..50208e28a
--- /dev/null
+++ b/kernel/opaqueproof.ml
@@ -0,0 +1,112 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Term
+open Mod_subst
+
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context } 
+type proofterm = (constr * Univ.constraints) Future.computation
+type opaque =
+  | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
+  | Direct of cooking_info list * proofterm
+  | NoIndirect of substitution list * proofterm
+
+(* hooks *)
+let default_get_opaque dp _ =
+  Errors.error
+    ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
+let default_get_univ dp _ =
+  Errors.error
+    ("Cannot access universe constraints of opaque proofs in library " ^
+    DirPath.to_string dp)
+let default_mk_indirect _ = None
+let default_join_indirect_local_opaque _ _ = ()
+let default_join_indirect_local_univ _ _ = ()
+
+let get_opaque = ref default_get_opaque
+let get_univ = ref default_get_univ
+let join_indirect_local_opaque = ref default_join_indirect_local_opaque
+let join_indirect_local_univ = ref default_join_indirect_local_univ
+let mk_indirect = ref default_mk_indirect
+
+let set_indirect_opaque_accessor f = (get_opaque := f)
+let set_indirect_univ_accessor f = (get_univ := f)
+let set_indirect_creator f = (mk_indirect := f)
+let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
+let set_join_indirect_local_univ f = join_indirect_local_univ := f
+let reset_indirect_creator () = mk_indirect := default_mk_indirect
+(* /hooks *)
+
+let create cu = Direct ([],cu)
+
+let turn_indirect o = match o with
+  | Indirect _
+  | NoIndirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
+  | Direct (d,cu) ->
+      let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
+      match !mk_indirect (d,cu) with
+      | None -> NoIndirect([],cu)
+      | Some (dp,i) -> Indirect ([],dp,i)
+
+let subst_opaque sub = function
+  | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
+  | NoIndirect (s,uc) -> NoIndirect (sub::s,uc)
+  | Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque")
+
+let iter_direct_opaque f = function
+  | Indirect _
+  | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+  | Direct (d,cu) ->
+      Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
+
+let discharge_direct_opaque ~cook_constr ci = function
+  | Indirect _
+  | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+  | Direct (d,cu) ->
+      Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
+
+let join_opaque = function
+  | Direct (_,cu) -> ignore(Future.join cu)
+  | NoIndirect (_,cu) -> ignore(Future.join cu)
+  | Indirect (_,dp,i) ->
+      !join_indirect_local_opaque dp i;
+      !join_indirect_local_univ dp i
+
+let force_proof = function
+  | Direct (_,cu) ->
+      fst(Future.force cu)
+  | NoIndirect (l,cu) ->
+      let c, _ = Future.force cu in
+      force_constr (List.fold_right subst_substituted l (from_val c))
+  | Indirect (l,dp,i) ->
+      let c = Future.force (!get_opaque dp i) in
+      force_constr (List.fold_right subst_substituted l (from_val c))
+
+let force_constraints = function
+  | Direct (_,cu)
+  | NoIndirect(_,cu) -> snd(Future.force cu)
+  | Indirect (_,dp,i) ->
+      match !get_univ dp i with
+      | None -> Univ.empty_constraint
+      | Some u -> Future.force u
+
+let get_constraints = function
+  | Direct (_,cu)
+  | NoIndirect(_,cu) -> Some(Future.chain ~pure:true cu snd)
+  | Indirect (_,dp,i) -> !get_univ dp i
+
+let get_proof = function
+  | Direct (_,cu) -> Future.chain ~pure:true cu fst
+  | NoIndirect(l,cu) ->
+      Future.chain ~pure:true cu (fun (c,_) ->
+        force_constr (List.fold_right subst_substituted l (from_val c)))
+  | Indirect (l,dp,i) ->
+      Future.chain ~pure:true (!get_opaque dp i) (fun c ->
+        force_constr (List.fold_right subst_substituted l (from_val c)))
diff --git a/kernel/lazyconstr.mli b/kernel/opaqueproof.mli
index db4d8fb72..957889aa9 100644
--- a/kernel/lazyconstr.mli
+++ b/kernel/opaqueproof.mli
@@ -10,52 +10,45 @@ open Names
 open Term
 open Mod_subst
 
-type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
-type cooking_info = { modlist : work_list; abstract : Context.named_context } 
-
-(** [constr_substituted] are [constr] with possibly pending
-    substitutions of kernel names. *)
-
-type constr_substituted
+(** This module implements the handling of opaque proof terms.
+    Opauqe proof terms are special since:
+    - they can be lazily computed and substituted
+    - they are stoked in an optionally loaded segment of .vo files
+    An [opaque] proof terms holds the real data until fully discharged.
+    In this case it is called [direct].
+    When it is [turn_indirect] the data is relocated to an opaque table
+    and the [opaque] is turned into an index. *)
 
-val from_val : constr -> constr_substituted
-val force : constr_substituted -> constr
-val subst_constr_subst :
-  substitution -> constr_substituted -> constr_substituted
-
-(** Opaque proof terms might be in some external tables. The
-    [force_opaque] function below allows to access these tables,
-    this might trigger the read of some extra parts of .vo files *)
-
-type lazy_constr
 type proofterm = (constr * Univ.constraints) Future.computation
+type opaque
 
-(** From a [constr] to some (immediate) [lazy_constr]. *)
-val opaque_from_val : proofterm -> lazy_constr
+(** From a [proofterm] to some [opaque]. *)
+val create : proofterm -> opaque
 
-(** Turn an immediate [lazy_constr] into an indirect one, thanks
-    to the indirect opaque creator configured below. *)
-val turn_indirect : lazy_constr -> lazy_constr
+(** Turn a direct [opaque] into an indirect one, also hashconses constr *)
+val turn_indirect : opaque -> opaque
 
-(** From a [lazy_constr] back to a [constr]. This might use the
+(** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor configured below. *)
-val force_opaque : lazy_constr -> constr
-val force_opaque_w_constraints : lazy_constr -> constr * Univ.constraints
-val get_opaque_future_constraints :
-  lazy_constr -> Univ.constraints Future.computation option
-val get_opaque_futures :
-  lazy_constr ->
-    Term.constr Future.computation * Univ.constraints Future.computation
+val force_proof : opaque -> constr
+val force_constraints : opaque -> Univ.constraints
+val get_proof : opaque -> Term.constr Future.computation
+val get_constraints : opaque -> Univ.constraints Future.computation option
 
-val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
+val subst_opaque : substitution -> opaque -> opaque
+val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
 
-(* val hcons_lazy_constr : lazy_constr -> lazy_constr *)
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context } 
 
-(* Used to discharge the proof term. *)
-val iter_direct_lazy_constr : (constr -> unit) -> lazy_constr -> lazy_constr
-val discharge_direct_lazy_constr : work_list -> Context.named_context -> (constr -> constr) -> lazy_constr -> lazy_constr
+(* The type has two caveats:
+   1) cook_constr is defined after
+   2) we have to store the input in the [opaque] in order to be able to
+      discharge it when turning a .vi into a .vo *)
+val discharge_direct_opaque :
+  cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
 
-val join_lazy_constr : lazy_constr -> unit
+val join_opaque : opaque -> unit
 
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The following two functions activate
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a93415f92..241e9d565 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -283,8 +283,8 @@ let safe_push_named (id,_,_ as d) env =
 let push_named_def (id,de) senv =
   let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
   let c,cst' = match c with
-    | Def c -> Lazyconstr.force c, Univ.empty_constraint
-    | OpaqueDef c -> Lazyconstr.force_opaque_w_constraints c
+    | Def c -> Mod_subst.force_constr c, Univ.empty_constraint
+    | OpaqueDef o -> Opaqueproof.force_proof o, Opaqueproof.force_constraints o
     | _ -> assert false in
   let senv = add_constraints (Now cst') senv in
   let senv' = add_constraints (Now cst) senv in
@@ -321,7 +321,7 @@ let constraints_of_sfb = function
       match cb.const_body with
       | (Undef _ | Def _) -> []
       | OpaqueDef lc ->
-          match Lazyconstr.get_opaque_future_constraints lc with
+          match Opaqueproof.get_constraints lc with
           | None -> []
           | Some fc ->
               match Future.peek_val fc with
@@ -383,7 +383,7 @@ let add_constant dir l decl senv =
     | OpaqueDef lc when DirPath.is_empty dir ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
-      { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) }
+      { cb with const_body = OpaqueDef (Opaqueproof.turn_indirect lc) }
     | _ -> cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6cedb6ad2..af4468981 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -290,8 +290,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	    | Def lc1 ->
 	      (* NB: cb1 might have been strengthened and appear as transparent.
 		 Anyway [check_conv] will handle that afterwards. *)
-	      let c1 = Lazyconstr.force lc1 in
-	      let c2 = Lazyconstr.force lc2 in
+	      let c1 = Mod_subst.force_constr lc1 in
+	      let c2 = Mod_subst.force_constr lc2 in
 	      check_conv NotConvertibleBodyField cst conv env c1 c2))
    | IndType ((kn,i),mind1) ->
        ignore (Errors.error (
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f059ea1ae..c86c13e04 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -69,12 +69,12 @@ let handle_side_effects env body side_eff =
       match cb.const_body with
       | Undef _ -> assert false
       | Def b ->
-          let b = Lazyconstr.force b in
+          let b = Mod_subst.force_constr b in
           let b_ty = Typeops.type_of_constant_type env cb.const_type in
           let t = sub c 1 (Vars.lift 1 t) in
           mkLetIn (cname c, b, b_ty, t)
       | OpaqueDef b -> 
-          let b = Lazyconstr.force_opaque b in
+          let b = Opaqueproof.force_proof b in
           let b_ty = Typeops.type_of_constant_type env cb.const_type in
           let t = sub c 1 (Vars.lift 1 t) in
           mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
@@ -108,7 +108,7 @@ let infer_declaration env dcl =
           let _typ, cst = constrain_type env j cst (`SomeWJ (typ,tyj,tycst)) in
           feedback_completion_typecheck feedback_id;
           j.uj_val, cst) in
-      let def = OpaqueDef (Lazyconstr.opaque_from_val proofterm) in
+      let def = OpaqueDef (Opaqueproof.create proofterm) in
       let typ = NonPolymorphicType typ in
       def, typ, tycst, c.const_entry_inline_code, c.const_entry_secctx
   | DefinitionEntry c ->
@@ -120,7 +120,7 @@ let infer_declaration env dcl =
       let j = hcons_j j in
       let typ, cst = constrain_type env j cst (map_option_typ typ) in
       feedback_completion_typecheck feedback_id;
-      let def = Def (Lazyconstr.from_val j.uj_val) in
+      let def = Def (Mod_subst.from_val j.uj_val) in
       def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
 
 let global_vars_set_constant_type env = function
@@ -159,9 +159,9 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
         let ids_typ = global_vars_set_constant_type env typ in
         let ids_def = match def with
         | Undef _ -> Idset.empty
-        | Def cs -> global_vars_set env (Lazyconstr.force cs)
+        | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
-            let vars = global_vars_set env (Lazyconstr.force_opaque lc) in
+            let vars = global_vars_set env (Opaqueproof.force_proof lc) in
             !suggest_proof_using kn env vars ids_typ context_ids;
             if !Flags.compilation_mode = Flags.BuildVo then
               record_aux env ids_typ vars;
@@ -179,12 +179,12 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
             let ids_typ = global_vars_set_constant_type env typ in
-            let ids_def = global_vars_set env (Lazyconstr.force cs) in
+            let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
             let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
-            OpaqueDef (Lazyconstr.iter_direct_lazy_constr (fun c ->
+            OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
               let ids_typ = global_vars_set_constant_type env typ in
               let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
diff --git a/library/declare.ml b/library/declare.ml
index 477e96bd8..c0c4dd571 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -121,7 +121,7 @@ let open_constant i ((sp,kn), obj) =
     match (Global.lookup_constant con).const_body with
     | (Def _ | Undef _) -> ()
     | OpaqueDef lc ->
-        match Lazyconstr.get_opaque_future_constraints lc with
+        match Opaqueproof.get_constraints lc with
         | Some f when Future.is_val f -> Global.add_constraints (Future.force f)
         | _ -> ()
 
@@ -155,7 +155,7 @@ let discharge_constant ((sp, kn), obj) =
   let hyps = section_segment_of_constant con in
   let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
   let abstract = named_of_variable_context hyps in
-  let new_decl = GlobalRecipe{ from; info = { Lazyconstr.modlist; abstract }} in
+  let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
   Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -197,8 +197,8 @@ let declare_sideff se =
   let id_of c = Names.Label.to_id (Names.Constant.label c) in
   let pt_opaque_of cb =
     match cb with
-    | { const_body = Def sc } -> Lazyconstr.force sc, false
-    | { const_body = OpaqueDef fc } -> Lazyconstr.force_opaque fc, true
+    | { const_body = Def sc } -> Mod_subst.force_constr sc, false
+    | { const_body = OpaqueDef fc } -> Opaqueproof.force_proof fc, true
     | { const_body = Undef _ } -> anomaly(str"Undefined side effect")
   in
   let ty_of cb =
diff --git a/library/lib.ml b/library/lib.ml
index ee89bb997..331196565 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -385,7 +385,7 @@ type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap
 
 let sectab =
   Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
-		        Lazyconstr.work_list * abstr_list) list)
+		        Opaqueproof.work_list * abstr_list) list)
     ~name:"section-context"
 
 let add_section () =
diff --git a/library/lib.mli b/library/lib.mli
index 787dc969e..8975acd9a 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -187,7 +187,7 @@ val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
 
 (* discharging a constant in one go *)
-val full_replacement_context : unit -> Lazyconstr.work_list list
+val full_replacement_context : unit -> Opaqueproof.work_list list
 val full_section_segment_of_constant :
   Names.constant -> (Context.named_context -> Context.named_context) list
 
diff --git a/library/library.ml b/library/library.ml
index c40f9d204..ccf282175 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -361,7 +361,7 @@ module OpaqueTables = struct
 
  let a_constr = Future.from_val (Term.mkRel 1)
  let a_univ = Future.from_val Univ.empty_constraint
- let a_discharge : Lazyconstr.cooking_info list = []
+ let a_discharge : Opaqueproof.cooking_info list = []
 
  let local_opaque_table = ref (Array.make 100 a_constr)
  let local_univ_table = ref (Array.make 100 a_univ)
@@ -424,17 +424,18 @@ module OpaqueTables = struct
 
 end
 
-let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque
-let _ = Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ
-let _ = Lazyconstr.set_join_indirect_local_opaque OpaqueTables.join_local_opaque
-let _ = Lazyconstr.set_join_indirect_local_univ OpaqueTables.join_local_univ
+let () =
+  Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque;
+  Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ;
+  Opaqueproof.set_join_indirect_local_opaque OpaqueTables.join_local_opaque;
+  Opaqueproof.set_join_indirect_local_univ OpaqueTables.join_local_univ
 
 (************************************************************************)
 (* Internalise libraries *)
 
 type seg_lib = library_disk
 type seg_univ = Univ.constraints Future.computation array
-type seg_discharge = Lazyconstr.cooking_info list array
+type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
 let mk_library md digest =
@@ -658,7 +659,7 @@ let start_library f =
   let id = Id.of_string (Filename.basename f) in
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
-  Lazyconstr.set_indirect_creator OpaqueTables.store;
+  Opaqueproof.set_indirect_creator OpaqueTables.store;
   Declaremods.start_library ldir;
   ldir,longf
 
@@ -714,12 +715,12 @@ let save_library_to ?todo dir f =
     | Some d ->
         assert(!Flags.compilation_mode = Flags.BuildVi);
         f ^ "i", (fun x -> Some (d x)), (fun x -> Some x), (fun x -> Some x) in
-  Lazyconstr.reset_indirect_creator ();
+  Opaqueproof.reset_indirect_creator ();
   (* HACK: end_library resets Lib and then joins the safe env.  To join the
    * env one needs to access the futures stored in the tables.  Standard
    * accessors use Lib.  Hence *)
-  Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib;
-  Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ_nolib;
+  Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib;
+  Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ_nolib;
   let cenv, seg, ast = Declaremods.end_library dir in
   let opaque_table, univ_table, disch_table, f2t_map =
     OpaqueTables.dump () in
diff --git a/library/library.mli b/library/library.mli
index ec39059e9..69fd5e940 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -33,7 +33,7 @@ val require_library_from_file :
 (** Segments of a library *)
 type seg_lib
 type seg_univ = Univ.constraints Future.computation array
-type seg_discharge = Lazyconstr.cooking_info list array
+type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
 (** Open a module (or a library); if the boolean is true then it's also
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5f17e0997..791294902 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -137,7 +137,7 @@ let check_arity env cb =
 let check_fix env cb i =
   match cb.const_body with
     | Def lbody ->
-	(match kind_of_term (Lazyconstr.force lbody) with
+	(match kind_of_term (Mod_subst.force_constr lbody) with
 	  | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6fc1973d0..134e01ee1 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -285,7 +285,7 @@ let rec extract_type env db j c args =
 		  | Undef _ | OpaqueDef _ -> mlt
 		  | Def _ when is_custom r -> mlt
 		  | Def lbody ->
-		      let newc = applist (Lazyconstr.force lbody, args) in
+		      let newc = applist (Mod_subst.force_constr lbody, args) in
 		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
 		      (* reduction, so [mlt] and [mlt'] might be different: *)
@@ -299,7 +299,7 @@ let rec extract_type env db j c args =
 		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
 		  | Def lbody ->
 		      (* We try to reduce. *)
-		      let newc = applist (Lazyconstr.force lbody, args) in
+		      let newc = applist (Mod_subst.force_constr lbody, args) in
 		      extract_type env db j newc []))
     | Ind (kn,i) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
@@ -523,7 +523,7 @@ and mlt_env env r = match r with
 	   | Def l_body ->
 	       (match flag_of_type env typ with
 		  | Info,TypeScheme ->
-		      let body = Lazyconstr.force l_body in
+		      let body = Mod_subst.force_constr l_body in
 		      let s,vl = type_sign_vl env typ in
 		      let db = db_from_sign s in
 		      let t = extract_type_scheme env db body (List.length s)
@@ -995,20 +995,20 @@ let extract_constant env kn cb =
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (Lazyconstr.force c)
+	  | Def c -> mk_typ (Mod_subst.force_constr c)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
-              mk_typ (Lazyconstr.force_opaque c)
+              mk_typ (Opaqueproof.force_proof c)
             else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (Lazyconstr.force c)
+	  | Def c -> mk_def (Mod_subst.force_constr c)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
-              mk_def (Lazyconstr.force_opaque c)
+              mk_def (Opaqueproof.force_proof c)
             else mk_ax ())
 
 let extract_constant_spec env kn cb =
@@ -1023,7 +1023,7 @@ let extract_constant_spec env kn cb =
 	  | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
 	  | Def body ->
 	      let db = db_from_sign s in
-              let body = Lazyconstr.force body in
+              let body = Mod_subst.force_constr body in
 	      let t = extract_type_scheme env db body (List.length s)
 	      in Stype (r, vl, Some t))
     | (Info, Default) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index da230ee0d..031db5b0c 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -531,11 +531,11 @@ let print_full_pure_context () =
 	      | OpaqueDef lc ->
 		str "Theorem " ++ print_basename con ++ cut () ++
 		str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
-		str "Proof " ++ pr_lconstr (Lazyconstr.force_opaque lc)
+		str "Proof " ++ pr_lconstr (Opaqueproof.force_proof lc)
 	      | Def c ->
 		str "Definition " ++ print_basename con ++ cut () ++
 		str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
-		pr_lconstr (Lazyconstr.force c))
+		pr_lconstr (Mod_subst.force_constr c))
           ++ str "." ++ fnl () ++ fnl ()
       | "INDUCTIVE" ->
 	  let mind = Global.mind_of_delta_kn kn in
diff --git a/printing/printmod.ml b/printing/printmod.ml
index b5f84c79e..34224d7b5 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -153,7 +153,7 @@ let print_body is_impl env mp (l,body) =
 	      | Def l when is_impl ->
 		spc () ++
 		hov 2 (str ":= " ++
-		       Printer.pr_lconstr_env env (Lazyconstr.force l))
+		       Printer.pr_lconstr_env env (Mod_subst.force_constr l))
 	      | _ -> mt ()) ++
             str ".")
     | SFBmind mib ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 07c91c8d5..f0ea69533 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -135,8 +135,8 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
 
 let constr_of_def = function
   | Declarations.Undef _ -> assert false
-  | Declarations.Def cs -> Lazyconstr.force cs
-  | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque lc
+  | Declarations.Def cs -> Mod_subst.force_constr cs
+  | Declarations.OpaqueDef lc -> Opaqueproof.force_proof lc
 
 let build_by_tactic env typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index aa64e3f22..6f696f27a 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -10,7 +10,7 @@ open Context
 open Cooking
 open Declarations
 open Entries
-open Lazyconstr
+open Opaqueproof
 
 val process_inductive :
   named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 9b07b4fcd..9a86d7ea0 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -830,7 +830,7 @@ end = struct (* {{{ *)
           List.iter (fun (_,se) -> Declareops.iter_side_effects (function
             | Declarations.SEsubproof(_,
                { Declarations.const_body = Declarations.OpaqueDef f } ) ->
-               Lazyconstr.join_lazy_constr f
+               Opaqueproof.join_opaque f
             | _ -> ())
           se) l;
           l) in
@@ -888,7 +888,8 @@ end = struct (* {{{ *)
         let c = Global.lookup_constant con in
         match c.Declarations.const_body with
         | Declarations.OpaqueDef lc ->
-            let pr, uc = Lazyconstr.get_opaque_futures lc in
+            let uc = Option.get (Opaqueproof.get_constraints lc) in
+            let pr = Opaqueproof.get_proof lc in
             let pr = Future.chain ~greedy:true ~pure:true pr discharge in
             let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
             ignore(Future.join pr);