Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks

 The recent experiment with -dont-load-proofs in the stdlib showed that
 this options isn't fully safe: some axioms were generated (Include ?
 functor application ? This is still to be fully understood).

 Instead, I've implemented an idea of Yann: only load opaque proofs when
 we need them. This is almost as fast as -dont-load-proofs (on the stdlib,
 we're now 15% faster than before instead of 20% faster with -dont-load-proofs),
 but fully compatible with Coq standard behavior.

 Technically, the const_body field of Declarations.constant_body now regroup
 const_body + const_opaque + const_inline in a ternary type. It is now either:
  - Undef : an axiom or parameter, with an inline info
  - Def : a transparent definition, with a constr_substituted
  - OpaqueDef : an opaque definition, with a lazy constr_substitued
 Accessing the lazy constr of an OpaqueDef might trigger the read on disk of
 the final section of a .vo, where opaque proofs are located.

 Some functions (body_of_constant, is_opaque, constant_has_body) emulate
 the behavior of the old fields. The rest of Coq (including the checker)
 has been adapted accordingly, either via direct access to the new const_body
 or via these new functions. Many places look nicer now (ok, subjective notion).

 There are now three options: -lazy-load-proofs (default), -force-load-proofs
 (earlier semantics), -dont-load-proofs. Note that -outputstate now implies
 -force-load-proofs (otherwise the marshaling fails on some delayed lazy).

 On the way, I fixed what looked like a bug : a module type
 (T with Definition x := c) was accepted even when x in T was opaque.
 I also tried to clarify Subtyping.check_constant.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 291 insertions, 213 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 337b907512..bd12528c79 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -714,11 +714,9 @@ let compile env c =
   Format.print_flush();  *)
   init_code,!fun_code, Array.of_list fv
 
-let compile_constant_body env body opaque =
-  if opaque then BCconstant
-  else match body with
-  | None -> BCconstant
-  | Some sb ->
+let compile_constant_body env = function
+  | Undef _ | OpaqueDef _ -> BCconstant
+  | Def sb ->
       let body = Declarations.force sb in
       match kind_of_term body with
 	| Const kn' ->
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 403c1c7b5b..74fb3f7ffe 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -9,9 +9,7 @@ open Pre_env
 val compile : env -> constr -> bytecodes * bytecodes * fv
                               (** init, fun, fv *)
 
-val compile_constant_body :
-    env -> constr_substituted option -> bool -> body_code
-                                 (** opaque *)
+val compile_constant_body : env -> constant_def -> body_code
 
 
 (** spiwack: this function contains the information needed to perform
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 87474b863f..02330339dd 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -117,16 +117,24 @@ type recipe = {
   d_abstract : named_context;
   d_modlist : work_list }
 
-let on_body f =
-  Option.map (fun c -> Declarations.from_val (f (Declarations.force c)))
+let on_body f = function
+  | Undef inl -> Undef inl
+  | Def cs -> Def (Declarations.from_val (f (Declarations.force cs)))
+  | OpaqueDef lc ->
+    OpaqueDef (Declarations.opaque_from_val (f (Declarations.force_opaque lc)))
+
+let constr_of_def = function
+  | Undef _ -> assert false
+  | Def cs -> Declarations.force cs
+  | OpaqueDef lc -> Declarations.force_opaque lc
 
 let cook_constant env r =
   let cb = r.d_from in
   let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
-  let body =
-    on_body (fun c ->
-      abstract_constant_body (expmod_constr r.d_modlist c) hyps)
-      cb.const_body in
+  let body = on_body
+    (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps)
+    cb.const_body
+  in
   let typ = match cb.const_type with
     | NonPolymorphicType t ->
 	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
@@ -134,7 +142,7 @@ let cook_constant env r =
     | PolymorphicArity (ctx,s) ->
 	let t = mkArity (ctx,Type s.poly_level) in
 	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
-	let j = make_judge (force (Option.get body)) typ in
+	let j = make_judge (constr_of_def body) typ in
 	Typeops.make_polymorphic_if_constant_for_ind env j
   in
-  (body, typ, cb.const_constraints, cb.const_opaque, None)
+  (body, typ, cb.const_constraints)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 4b8b4537cb..5f31ff8ce6 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -22,8 +22,7 @@ type recipe = {
   d_modlist : work_list }
 
 val cook_constant :
-  env -> recipe ->
-    constr_substituted option * constant_type * constraints * bool * inline
+  env -> recipe -> constant_def * constant_type * constraints
 
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index fc8064d59f..f092c82616 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -49,17 +49,64 @@ let force = force subst_mps
 
 let subst_constr_subst = subst_substituted
 
-type inline = int option (* inlining level, None for no inlining *)
+(** Opaque proof terms are not loaded immediately, but are there
+    in a lazy form. Forcing this lazy may trigger some unmarshal of
+    the necessary structure. The ['a substituted] type isn't really great
+    here, so we store "manually" a substitution list, the younger one at top.
+*)
+
+type lazy_constr = constr_substituted Lazy.t * substitution list
+
+let force_lazy_constr (c,l) =
+  List.fold_right subst_constr_subst l (Lazy.force c)
+
+let lazy_constr_is_val (c,_) = Lazy.lazy_is_val c
+
+let make_lazy_constr c = (c, [])
+
+let force_opaque lc = force (force_lazy_constr lc)
+
+let opaque_from_val c = (Lazy.lazy_from_val (from_val c), [])
+
+let subst_lazy_constr sub (c,l) = (c,sub::l)
+
+(** Inlining level of parameters at functor applications.
+    None means no inlining *)
+
+type inline = int option
+
+(** A constant can have no body (axiom/parameter), or a
+    transparent body, or an opaque one *)
+
+type constant_def =
+  | Undef of inline
+  | Def of constr_substituted
+  | OpaqueDef of lazy_constr
+
+let subst_constant_def sub = function
+  | Undef inl -> Undef inl
+  | Def c -> Def (subst_constr_subst sub c)
+  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
 
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
-    const_body : constr_substituted option;
+    const_body : constant_def;
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted;
-   (* const_type_code : Cemitcodes.to_patch; *)
-    const_constraints : constraints;
-    const_opaque : bool;
-    const_inline : inline }
+    const_constraints : constraints }
+
+let body_of_constant cb = match cb.const_body with
+  | Undef _ -> None
+  | Def c -> Some c
+  | OpaqueDef lc -> Some (force_lazy_constr lc)
+
+let constant_has_body cb = match cb.const_body with
+  | Undef _ -> false
+  | Def _ | OpaqueDef _ -> true
+
+let is_opaque cb = match cb.const_body with
+  | OpaqueDef _ -> true
+  | Undef _ | Def _ -> false
 
 (*s Inductive types (internal representation with redundant
     information). *)
@@ -218,14 +265,12 @@ let subst_arity sub arity =
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 let subst_const_body sub cb = {
   const_hyps = (assert (cb.const_hyps=[]); []);
-  const_body = Option.map (subst_constr_subst sub) cb.const_body;
+  const_body = subst_constant_def sub cb.const_body;
   const_type = subst_arity sub cb.const_type;
   const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
   (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
-  const_constraints = cb.const_constraints;
-  const_opaque = cb.const_opaque;
-  const_inline = cb.const_inline} 
-  
+  const_constraints = cb.const_constraints}
+
 let subst_arity sub = function
 | Monomorphic s ->
     Monomorphic {
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index d4c86fb353..ebedd17e67 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -35,20 +35,54 @@ type constr_substituted
 val from_val : constr -> constr_substituted
 val force : constr_substituted -> constr
 
-type inline = int option (* inlining level, None for no inlining *)
+(** Opaque proof terms are not loaded immediately, but are there
+    in a lazy form. Forcing this lazy may trigger some unmarshal of
+    the necessary structure. *)
+
+type lazy_constr
+
+val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
+val force_lazy_constr : lazy_constr -> constr_substituted
+val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr
+val lazy_constr_is_val : lazy_constr -> bool
+
+val force_opaque : lazy_constr -> constr
+val opaque_from_val : constr -> lazy_constr
+
+(** Inlining level of parameters at functor applications.
+    None means no inlining *)
+
+type inline = int option
+
+(** A constant can have no body (axiom/parameter), or a
+    transparent body, or an opaque one *)
+
+type constant_def =
+  | Undef of inline
+  | Def of constr_substituted
+  | OpaqueDef of lazy_constr
+
+val subst_constant_def : substitution -> constant_def -> constant_def
 
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
-    const_body : constr_substituted option;
+    const_body : constant_def;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
-   (* const_type_code : to_patch;*)
-    const_constraints : constraints;
-    const_opaque : bool;
-    const_inline : inline }
+    const_constraints : constraints }
 
 val subst_const_body : substitution -> constant_body -> constant_body
 
+(** Is there a actual body in const_body or const_body_opaque ? *)
+
+val constant_has_body : constant_body -> bool
+
+(** Accessing const_body_opaque or const_body *)
+
+val body_of_constant : constant_body -> constr_substituted option
+
+val is_opaque : constant_body -> bool
+
 (** {6 Representation of mutual inductive types in the kernel } *)
 
 type recarg =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 34074b677e..a69a98c1bf 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -170,10 +170,10 @@ exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env kn =
   let cb = lookup_constant kn env in
-  if cb.const_opaque then raise (NotEvaluableConst Opaque);
   match cb.const_body with
-    | Some l_body -> Declarations.force l_body
-    | None -> raise (NotEvaluableConst NoBody)
+    | Def l_body -> Declarations.force l_body
+    | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+    | Undef _ -> raise (NotEvaluableConst NoBody)
 
 let constant_opt_value env cst =
   try Some (constant_value env cst)
@@ -648,14 +648,14 @@ let assumptions ?(add_opaque=false) st (* t env *) =
 	(s,ContextObjectMap.add cst ctype acc)
     in
     let (s,acc) =
-      if cb.Declarations.const_body <> None
-	&& (cb.Declarations.const_opaque || not (Cpred.mem kn knst))
+      if Declarations.constant_has_body cb
+	&& (Declarations.is_opaque cb || not (Cpred.mem kn knst))
 	&& add_opaque
       then
 	do_type (Opaque kn)
       else (s,acc)
     in
-      match cb.Declarations.const_body with
+      match Declarations.body_of_constant cb with
       | None -> do_type (Axiom kn)
       | Some body -> aux (Declarations.force body) env s acc
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f26d49dde4..af1e175914 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -189,9 +189,7 @@ type unsafe_type_judgment = {
 
 (** {6 Compilation of global declaration } *)
 
-val compile_constant_body :
-    env -> constr_substituted option -> bool -> Cemitcodes.body_code
-                                 (** opaque *)
+val compile_constant_body : env -> constant_def -> Cemitcodes.body_code
 
 exception Hyp_not_found
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 335c2a94ee..aad541d218 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -84,40 +84,41 @@ and check_with_aux_def env sign with_decl mp equiv =
           | With_Definition ([],_) -> assert false
 	  | With_Definition ([id],c) ->
 	      let cb = match spec with
-		  SFBconst cb -> cb
+		| SFBconst cb -> cb
 		| _ -> error_not_a_constant l
 	      in
-		begin
-		  match cb.const_body with
-		    | None ->
-			let (j,cst1) = Typeops.infer env' c in
-			let typ = Typeops.type_of_constant_type env' cb.const_type in
-			let cst2 = Reduction.conv_leq env' j.uj_type typ in
-			let cst =
-			  union_constraints
-			    (union_constraints cb.const_constraints cst1)
-			    cst2 in
-			let body = Some (Declarations.from_val j.uj_val) in
-			let cb' = {cb with
-				     const_body = body;
-				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false);
-                                     const_constraints = cst} in
-			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
-		    | Some b ->
-			let cst1 = Reduction.conv env' c (Declarations.force b) in
-			let cst = union_constraints cb.const_constraints cst1 in
-			let body = Some (Declarations.from_val c) in
-			let cb' = {cb with
-				     const_body = body;
-				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false);
-                                     const_constraints = cst} in
-			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
-	      end
+	      let def,cst = match cb.const_body with
+		| Undef _ ->
+		    let (j,cst1) = Typeops.infer env' c in
+		    let typ = Typeops.type_of_constant_type env' cb.const_type in
+		    let cst2 = Reduction.conv_leq env' j.uj_type typ in
+		    let cst =
+		      union_constraints
+			(union_constraints cb.const_constraints cst1)
+			cst2
+		    in
+		    let def = Def (Declarations.from_val j.uj_val) in
+		    def,cst
+		| Def cs ->
+		    let cst1 = Reduction.conv env' c (Declarations.force cs) in
+		    let cst = union_constraints cb.const_constraints cst1 in
+		    let def = Def (Declarations.from_val c) in
+		    def,cst
+		| OpaqueDef _ ->
+		    (* We cannot make transparent an opaque field *)
+		    raise Reduction.NotConvertible
+	      in
+	      let cb' =
+		{ cb with
+		  const_body = def;
+		  const_body_code =
+		    Cemitcodes.from_val (compile_constant_body env' def);
+		  const_constraints = cst }
+	      in
+	      SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
 	  | With_Definition (_::_,c) ->
 	      let old = match spec with
-		  SFBmodule msb -> msb
+		| SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
 	      in
 		begin
@@ -136,7 +137,7 @@ and check_with_aux_def env sign with_decl mp equiv =
 		end
 	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
-	Not_found -> error_no_such_label l
+      | Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_incorrect_with_constraint l
 
 and check_with_aux_mod env sign with_decl mp equiv = 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 6d4ebb989b..df9b7e81f6 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -290,21 +290,17 @@ and add_module mb env =
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 let strengthen_const env mp_from l cb resolver = 
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _ 
-  | _, None ->
+  match cb.const_body with
+    | Def _ -> cb
+    | _ ->
       let con = make_con mp_from empty_dirpath l in
       let con =  constant_of_delta resolver con in
       let const = mkConst con in 
-      let const_subs = Some (Declarations.from_val const) in
-	{cb with 
-	   const_body = const_subs;
-	   const_opaque = false;
-	   const_body_code = Cemitcodes.from_val
-            (compile_constant_body env const_subs false)
-	}
-	  
+      let def = Def (Declarations.from_val const) in
+      { cb with
+	const_body = def;
+	const_body_code = Cemitcodes.from_val (compile_constant_body env def)
+      }
 
 let rec strengthen_mod env mp_from mp_to mb = 
   if mp_in_delta mb.mod_mp mb.mod_delta then
@@ -401,10 +397,9 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	try
 	  let constant = lookup_constant con' env in
 	  let l = make_inline delta r in
-	  if constant.Declarations.const_opaque then l
-	  else match constant.Declarations.const_body with
-	    | None -> l
-	    | Some body ->
+	  match constant.const_body with
+	    | Undef _ | OpaqueDef _ -> l
+	    | Def body ->
 	      let constr = Declarations.force body in
 	      add_inline_constr_delta_resolver con lev constr l
 	with Not_found ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8f4ec76f84..bdffa68022 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -253,21 +253,27 @@ type global_declaration =
   | ConstantEntry of constant_entry
   | GlobalRecipe of Cooking.recipe
 
-let hcons_constant_type = function
+let hcons_const_type = function
   | NonPolymorphicType t ->
       NonPolymorphicType (hcons1_constr t)
   | PolymorphicArity (ctx,s) ->
       PolymorphicArity (map_rel_context hcons1_constr ctx,s)
 
+let hcons_const_body = function
+  | Undef inl -> Undef inl
+  | Def l_constr ->
+    let constr = Declarations.force l_constr in
+    Def (Declarations.from_val (hcons1_constr constr))
+  | OpaqueDef lc ->
+    if lazy_constr_is_val lc then
+      let constr = Declarations.force_opaque lc in
+      OpaqueDef (Declarations.opaque_from_val (hcons1_constr constr))
+    else OpaqueDef lc
+
 let hcons_constant_body cb =
-  let body = match cb.const_body with
-      None -> None
-    | Some l_constr -> let constr = Declarations.force l_constr in
-	Some (Declarations.from_val (hcons1_constr constr))
-  in
-    { cb with
-	const_body = body;
-	const_type = hcons_constant_type cb.const_type }
+  { cb with
+    const_body = hcons_const_body cb.const_body;
+    const_type = hcons_const_type cb.const_type }
 
 let add_constant dir l decl senv =
   check_label l senv.labset;
@@ -280,9 +286,10 @@ let add_constant dir l decl senv =
 	    if dir = empty_dirpath then hcons_constant_body cb else cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
-  let senv'' = match cb.const_inline with
-    | None -> senv'
-    | Some lev -> update_resolver (add_inline_delta_resolver kn lev) senv'
+  let senv'' = match cb.const_body with
+    | Undef (Some lev) ->
+      update_resolver (add_inline_delta_resolver kn lev) senv'
+    | _ -> senv'
   in
   kn, senv''
 
@@ -768,15 +775,20 @@ module LightenLibrary : sig
   type table 
   type lightened_compiled_library 
   val save : compiled_library -> lightened_compiled_library * table
-  val load : load_proof:bool -> (unit -> table) 
+  val load : load_proof:Flags.load_proofs -> table Lazy.t
     -> lightened_compiled_library -> compiled_library
 end = struct
 
   (* The table is implemented as an array of [constr_substituted].
-     Thus, its keys are integers which can be easily embedded inside
-     [constr_substituted]. This way the [compiled_library] type does
-     not have to be changed. *)
+     Keys are hence integers. To avoid changing the [compiled_library]
+     type, we brutally encode integers into [lazy_constr]. This isn't
+     pretty, but shouldn't be dangerous since the produced structure
+     [lightened_compiled_library] is abstract and only meant for writing
+     to .vo via Marshal (which doesn't care about types).
+  *)
   type table = constr_substituted array
+  let key_as_lazy_constr (i:int) = (Obj.magic i : lazy_constr)
+  let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int)
 
   (* To avoid any future misuse of the lightened library that could 
      interpret encoded keys as real [constr_substituted], we hide 
@@ -806,9 +818,9 @@ end = struct
 	    }    
     and traverse_struct struc =
       let traverse_body (l,body) = (l,match body with
-	| SFBconst ({const_opaque=true} as x) -> 
-	  SFBconst {x with const_body = on_opaque_const_body x.const_body }
-	| (SFBconst _ | SFBmind _ ) as x -> 
+	| SFBconst cb when is_opaque cb ->
+	  SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
+	| (SFBconst _ | SFBmind _ ) as x ->
 	  x
 	| SFBmodule m -> 
 	  SFBmodule (traverse_module m)
@@ -837,31 +849,29 @@ end = struct
      traverse it and add an indirection between the module body 
      and its reference to a [const_body]. *)
   let save library = 
-    let ((insert    : constr_substituted -> constr_substituted), 
+    let ((insert    : constant_def -> constant_def),
 	 (get_table : unit -> table)) = 
       (* We use an integer as a key inside the table. *)
       let counter = ref (-1) in
-      (* ... but it is wrapped inside a [constr_substituted]. *)
-      let key_as_constr key = Declarations.from_val (Term.mkRel key) in
 
       (* During the traversal, the table is implemented by a list 
 	 to get constant time insertion. *)
       let opaque_definitions = ref [] in
       
       ((* Insert inside the table. *) 
-	(fun opaque_definition -> 
-	incr counter; 
-	opaque_definitions := opaque_definition :: !opaque_definitions;
-	key_as_constr !counter), 
+	(fun def ->
+	  let opaque_definition = match def with
+	    | OpaqueDef lc -> force_lazy_constr lc
+	    | _ -> assert false
+	  in
+	  incr counter;
+	  opaque_definitions := opaque_definition :: !opaque_definitions;
+	  OpaqueDef (key_as_lazy_constr !counter)),
 
        (* Get the final table representation. *)
        (fun () -> Array.of_list (List.rev !opaque_definitions)))
     in
-    let encode_const_body : constr_substituted option -> constr_substituted option = function
-      | None -> None
-      | Some ct -> Some (insert ct)
-    in
-    let lightened_library = traverse_library encode_const_body library in
+    let lightened_library = traverse_library insert library in
     (lightened_library, get_table ())
 
   (* Loading is also a traversing that decodes the embedded keys that
@@ -870,19 +880,24 @@ end = struct
      [constr_substituted]. Otherwise, we set the [const_body] field
      to [None]. 
   *)
-  let load ~load_proof (get_table : unit -> table) lightened_library = 
-    let decode_key : constr_substituted option -> constr_substituted option = 
-      if load_proof then 
-	let table = get_table () in
-	function Some cterm -> 
-	  Some (try 
-		  table.(Term.destRel (Declarations.force cterm))
-	    with _ -> 
-	      assert false
-	  )
-	  | _ -> None
-      else 
-	fun _ -> None
+  let load ~load_proof (table : table Lazy.t) lightened_library =
+    let decode_key = function
+      | Undef _ | Def _ -> assert false
+      | OpaqueDef k ->
+	  let k = key_of_lazy_constr k in
+	  let access key =
+	    try (Lazy.force table).(key)
+	    with _ -> error "Error while retrieving an opaque body"
+	  in
+	  match load_proof with
+	    | Flags.Force ->
+	      let lc = Lazy.lazy_from_val (access k) in
+	      OpaqueDef (make_lazy_constr lc)
+	    | Flags.Lazy ->
+	      let lc = lazy (access k) in
+	      OpaqueDef (make_lazy_constr lc)
+	    | Flags.Dont ->
+	      Undef None
     in
     traverse_library decode_key lightened_library
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 0ab70b69e8..3a79548741 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -114,10 +114,11 @@ val import : compiled_library -> Digest.t -> safe_environment
 
 module LightenLibrary :
 sig
-  type table 
-  type lightened_compiled_library 
+  type table
+  type lightened_compiled_library
   val save : compiled_library -> lightened_compiled_library * table
-  val load : load_proof:bool -> (unit -> table) -> lightened_compiled_library -> compiled_library
+  val load : load_proof:Flags.load_proofs -> table Lazy.t ->
+    lightened_compiled_library -> compiled_library
 end
 
 (** {6 Typing judgments } *)
@@ -135,8 +136,6 @@ val safe_infer : safe_environment -> constr -> judgment * Univ.constraints
 
 val typing : safe_environment -> constr -> judgment
 
-
-
 (*spiwack: safe retroknowledge functionalities *)
 
 open Retroknowledge
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 0c72995080..cac55f4be6 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -253,55 +253,46 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 
   match info1 with
     | Constant cb1 ->
-	assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
-	(*Start by checking types*)
-	let cb1 = subst_const_body subst1 cb1 in
-	let cb2 = subst_const_body subst2 cb2 in
+      assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
+      let cb1 = subst_const_body subst1 cb1 in
+      let cb2 = subst_const_body subst2 cb2 in
+      (* Start by checking types*)
       let typ1 = Typeops.type_of_constant_type env cb1.const_type in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = check_type cst env typ1 typ2 in
-      let con = make_con mp1 empty_dirpath l in
-      let cst =
-	if cb2.const_opaque then
-	  (* In this case we compare opaque definitions, we need to bypass
-	     the opacity and do a delta step*)
-	  match cb2.const_body with
-            | None -> cst
-            | Some lc2 ->
-		let c2 = Declarations.force lc2 in
-		let c1 = match cb1.const_body with
-		  | Some lc1 ->
-		      let c = Declarations.force lc1 in
-			begin
-			  match (kind_of_term c),(kind_of_term c2) with
-			      Const n1,Const n2 when (eq_constant n1 n2) -> c
-				(* c1 may have been strenghtened 
-				   we need to unfold it*)
-			    | Const n,_ ->
-				let cb = subst_const_body subst1
-				  (lookup_constant n env) in
-				  (match cb.const_opaque,
-				     cb.const_body with
-				       | true, Some lc1 ->
-					   Declarations.force lc1
-				       | _,_ -> c)
-			    | _ ,_-> c
-			end
-		  | None -> mkConst con
-		in
-		  check_conv NotConvertibleBodyField cst conv env c1 c2
-	else
-	  match cb2.const_body with
-            | None -> cst
-            | Some lc2 ->
-		let c2 = Declarations.force lc2 in
-		let c1 = match cb1.const_body with
-		  | Some lc1 -> Declarations.force lc1
-		  | None -> mkConst con
-		in
-		  check_conv NotConvertibleBodyField cst conv env c1 c2
-      in
-	cst
+      (* Now we check the bodies *)
+      (match cb2.const_body with
+	| Undef _ -> cst
+	| Def lc2 ->
+	  (* Only a transparent cb1 can implement a transparent cb2.
+	     NB: cb1 might have been strengthened and appear as transparent.
+	     Anyway [check_conv] will handle that afterwards. *)
+	  (match cb1.const_body with
+	    | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField
+	    | Def lc1 ->
+	      let c1 = Declarations.force lc1 in
+	      let c2 = Declarations.force lc2 in
+	      check_conv NotConvertibleBodyField cst conv env c1 c2)
+	| OpaqueDef lc2 ->
+	  (* Here cb1 can be either opaque or transparent. We need to
+	     bypass the opacity and possibly do a delta step. *)
+	  (match body_of_constant cb1 with
+	    | None -> error NotConvertibleBodyField
+	    | Some lc1 ->
+	      let c1 = Declarations.force lc1 in
+	      let c2 = Declarations.force_opaque lc2 in
+	      let c1' = match (kind_of_term c1),(kind_of_term c2) with
+		| Const n1,Const n2 when (eq_constant n1 n2) -> c1
+		  (* cb1 may have been strengthened, we need to unfold it: *)
+		| Const n1,_ ->
+		  let cb1' = subst_const_body subst1 (lookup_constant n1 env)
+		  in
+		  (match cb1'.const_body with
+		    | OpaqueDef lc1' -> Declarations.force_opaque lc1'
+		    | _ -> c1)
+		| _,_ -> c1
+	      in
+	      check_conv NotConvertibleBodyField cst conv env c1' c2))
    | IndType ((kn,i),mind1) ->
        ignore (Util.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -309,7 +300,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "inductive type and give a definition to map the old name to the new " ^
        "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
-      if cb2.const_body <> None then error DefinitionFieldExpected;
+      if constant_has_body cb2 then error DefinitionFieldExpected;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2
@@ -320,7 +311,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "constructor and give a definition to map the old name to the new " ^
        "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
-      if cb2.const_body <> None then error DefinitionFieldExpected;
+      if constant_has_body cb2 then error DefinitionFieldExpected;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv NotConvertibleTypeField cst conv env ty1 ty2
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 801bd6c807..8146ea7c16 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -93,12 +93,15 @@ let infer_declaration env dcl =
   | DefinitionEntry c ->
       let (j,cst) = infer env c.const_entry_body in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
-      Some (Declarations.from_val j.uj_val), typ, cst,
-        c.const_entry_opaque, None
+      let def =
+	if c.const_entry_opaque
+	then OpaqueDef (Declarations.opaque_from_val j.uj_val)
+	else Def (Declarations.from_val j.uj_val)
+      in
+      def, typ, cst
   | ParameterEntry (t,nl) ->
       let (j,cst) = infer env t in
-      None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
-        false, nl
+      Undef nl, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst
 
 let global_vars_set_constant_type env = function
   | NonPolymorphicType t -> global_vars_set env t
@@ -108,25 +111,20 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Idset.union (global_vars_set env t) c))
       ctx ~init:Idset.empty
 
-let build_constant_declaration env kn (body,typ,cst,op,inline) =
-  let ids =
-    match body with
-    | None -> global_vars_set_constant_type env typ
-    | Some b ->
-        Idset.union
-	  (global_vars_set env (Declarations.force b))
-	  (global_vars_set_constant_type env typ)
+let build_constant_declaration env kn (def,typ,cst) =
+  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 (Declarations.force cs)
+    | OpaqueDef lc -> global_vars_set env (Declarations.force_opaque lc)
   in
-  let tps = Cemitcodes.from_val (compile_constant_body env body op) in
-  let hyps = keep_hyps env ids in
-    { const_hyps = hyps;
-      const_body = body;
-      const_type = typ;
-      const_body_code = tps;
-     (* const_type_code = to_patch env typ;*)
-      const_constraints = cst;
-      const_opaque = op;
-      const_inline = inline}
+  let hyps = keep_hyps env (Idset.union ids_typ ids_def) in
+  let tps = Cemitcodes.from_val (compile_constant_body env def) in
+  { const_hyps = hyps;
+    const_body = def;
+    const_type = typ;
+    const_body_code = tps;
+    const_constraints = cst }
 
 (*s Global and local constant declaration. *)
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 8b48fc3cf7..158f2c7877 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,11 +22,10 @@ val translate_local_assum : env -> types ->
   types * Univ.constraints
 
 val infer_declaration : env -> constant_entry ->
-   constr_substituted option * constant_type * constraints * bool * inline
+  constant_def * constant_type * constraints
 
 val build_constant_declaration : env -> 'a ->
-    constr_substituted option * constant_type * constraints * bool * inline ->
-      constant_body
+  constant_def * constant_type * constraints -> constant_body
 
 val translate_constant : env -> constant -> constant_entry -> constant_body