aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-24 20:46:32 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-26 14:53:08 +0100
commit15b6c9b6fa268a9af6dd4f05961e469545e92a6f (patch)
tree2e5aacf72993b448d1e80b0cbfbf0a09091ecb32
parente6556db92d4c4fe9ba38f26b89f805095d2b2638 (diff)
Lazyconstr -> Opaqueproof
Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
-rw-r--r--dev/printers.mllib2
-rw-r--r--dev/top_printers.ml2
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/cooking.ml17
-rw-r--r--kernel/cooking.mli6
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/declareops.ml15
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/lazyconstr.ml134
-rw-r--r--kernel/mod_subst.ml3
-rw-r--r--kernel/mod_subst.mli4
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/modops.ml4
-rw-r--r--kernel/nativecode.ml4
-rw-r--r--kernel/nativelambda.ml4
-rw-r--r--kernel/opaqueproof.ml112
-rw-r--r--kernel/opaqueproof.mli (renamed from kernel/lazyconstr.mli)65
-rw-r--r--kernel/safe_typing.ml8
-rw-r--r--kernel/subtyping.ml4
-rw-r--r--kernel/term_typing.ml16
-rw-r--r--library/declare.ml8
-rw-r--r--library/lib.ml2
-rw-r--r--library/lib.mli2
-rw-r--r--library/library.ml21
-rw-r--r--library/library.mli2
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/extraction.ml16
-rw-r--r--printing/prettyp.ml4
-rw-r--r--printing/printmod.ml2
-rw-r--r--proofs/pfedit.ml4
-rw-r--r--toplevel/discharge.mli2
-rw-r--r--toplevel/stm.ml5
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);