Lazyconstr -> Opaqueproof

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

5 files changed, 18 insertions, 17 deletions

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