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

49 files changed, 591 insertions, 447 deletions

diff --git a/Makefile.build b/Makefile.build
index eefafb0cb..28da169cf 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -69,15 +69,9 @@ TIMECMD=	# is "'time -p'" to get compilation time of .v
 # For instance:
 # TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-# Since library files aren't meant to contain queries like Print Assumptions
-# nor extractions, it is safe (and quite quicker) to compile them with
-# -dont-load-proofs
-
-LOADPROOFS=-dont-load-proofs
-
 COQOPTS=$(COQ_XML) $(VM)
 BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)
-BOOTCOQC:=$(BOOTCOQTOP) $(LOADPROOFS) -compile
+BOOTCOQC:=$(BOOTCOQTOP) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
 # or only abbreviated versions. 
diff --git a/checker/check.ml b/checker/check.ml
index 3dc510dcc..bb42b949d 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -270,10 +270,10 @@ let with_magic_number_check f a =
 (************************************************************************)
 (* Internalise libraries *)
 
-let mk_library md f get_table digest = {
+let mk_library md f table digest = {
   library_name = md.md_name;
   library_filename = f;
-  library_compiled = Safe_typing.LightenLibrary.load ~load_proof:true get_table md.md_compiled;
+  library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled;
   library_deps = md.md_deps;
   library_digest = digest }
 
@@ -287,24 +287,21 @@ let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
   Flags.if_verbose msg (str"[intern "++str f++str" ...");
-  let (md,get_table,close,digest) =
+  let (md,table,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
       let (md:library_disk) = System.marshal_in ch in
       let digest = System.marshal_in ch in
-      let get_table () = 
-	(System.marshal_in ch : Safe_typing.LightenLibrary.table) 
-      in
+      let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
+      close_in ch;
       if dir <> md.md_name then
         errorlabstrm "load_physical_library"
           (name_clash_message dir md.md_name f);
       Flags.if_verbose msgnl(str" done]");
-      md,get_table,(fun () -> close_in ch),digest
+      md,table,digest
     with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
-  let library = mk_library md f get_table digest in
-  close ();
-  library
+  mk_library md f table digest
 
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 7ca406fec..5f28269ee 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -37,7 +37,7 @@ let cst_filter f csts =
     (fun c ce acc -> if f c ce then c::acc else acc)
     csts []
 
-let is_ax _ cb = cb.const_body = None
+let is_ax _ cb = not (constant_has_body cb)
 
 let pr_ax csts =
   let axs = cst_filter is_ax csts in
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 084b4eb54..890996d10 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -478,27 +478,67 @@ let val_cstr_subst = val_substituted val_constr
 
 let subst_constr_subst = subst_substituted
 
-type inline = int option (* inlining level, None for no inlining *)
+(** Beware! In .vo files, lazy_constr are stored as integers
+   used as indexes for a separate table. The actual lazy_constr is restored
+   later, by [Safe_typing.LightenLibrary.load]. This allows us
+   to use here a different definition of lazy_constr than coqtop:
+   since the checker will inspect all proofs parts, even opaque
+   ones, no need to use Lazy.t here *)
+
+type lazy_constr = constr_substituted
+let subst_lazy_constr = subst_substituted
+let force_lazy_constr = force_constr
+let lazy_constr_from_val c = c
+let val_lazy_constr = val_cstr_subst
+
+(** Inlining level of parameters at functor applications.
+    This is ignored by the checker. *)
+
+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 val_cst_def =
+  val_sum "constant_def" 0
+    [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_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 : to_patch_substituted;
-   (* const_type_code : Cemitcodes.to_patch; *)
-    const_constraints : Univ.constraints;
-    const_opaque : bool;
-    const_inline : inline }
+    const_constraints : Univ.constraints }
+
+let body_of_constant cb = match cb.const_body with
+  | Undef _ -> None
+  | Def c -> Some c
+  | OpaqueDef c -> Some c
+
+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
+  | Def _ | Undef _ -> false
 
 let val_cb = val_tuple ~name:"constant_body"
   [|val_nctxt;
-    val_opt val_cstr_subst;
+    val_cst_def;
     val_cst_type;
     no_val;
-    val_cstrs;
-    val_bool;
-    val_opt val_int |]
-
+    val_cstrs|]
 
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
@@ -662,13 +702,10 @@ let subst_arity sub = function
 (* 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 ->
diff --git a/checker/declarations.mli b/checker/declarations.mli
index b5038996c..90beb326b 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -29,16 +29,40 @@ type constr_substituted
 val force_constr : constr_substituted -> constr
 val from_val : constr -> constr_substituted
 
-type inline = int option (* inlining level, None for no inlining *)
+(** Beware! In .vo files, lazy_constr are stored as integers
+   used as indexes for a separate table. The actual lazy_constr is restored
+   later, by [Safe_typing.LightenLibrary.load]. This allows us
+   to use here a different definition of lazy_constr than coqtop:
+   since the checker will inspect all proofs parts, even opaque
+   ones, no need to use Lazy.t here *)
+
+type lazy_constr
+val force_lazy_constr : lazy_constr -> constr
+val lazy_constr_from_val : constr_substituted -> lazy_constr
+
+(** Inlining level of parameters at functor applications.
+    This is ignored by the checker. *)
+
+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
 
 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_constraints : Univ.constraints;
-    const_opaque : bool;
-    const_inline : inline }
+    const_constraints : Univ.constraints }
+
+val body_of_constant : constant_body -> constr_substituted option
+val constant_has_body : constant_body -> bool
+val is_opaque : constant_body -> bool
 
 (* Mutual inductives *)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index d960e2a7c..d79cb118b 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -124,10 +124,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 -> force_constr l_body
-    | None -> raise (NotEvaluableConst NoBody)
+    | Def l_body -> force_constr l_body
+    | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+    | Undef _ -> raise (NotEvaluableConst NoBody)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 30149331e..e6582e918 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -33,7 +33,7 @@ let check_constant_declaration env kn cb =
         let ty, cu = refresh_arity ty in
         let envty = add_constraints cu env' in
         let _ = infer_type envty ty in
-        (match cb.const_body with
+        (match body_of_constant cb with
           | Some bd ->
               let j = infer env' (force_constr bd) in
               conv_leq envty j ty
@@ -110,14 +110,17 @@ let check_definition_sub env cb1 cb2 =
   let typ1 = Typeops.type_of_constant_type env cb1.const_type in
   let typ2 = Typeops.type_of_constant_type env cb2.const_type in
   check_type env typ1 typ2;
-  (match cb2 with
-    | {const_body=Some lc2;const_opaque=false} ->
-	let c2 = force_constr lc2 in
-	let c1 = match cb1.const_body with
-	  | Some lc1 -> force_constr lc1
-	  | None -> assert false in
-	Reduction.conv env c1 c2
-    | _ -> ())
+  (match cb2.const_body with
+    | Undef _ -> ()
+    | Def lc2 ->
+	(match cb1.const_body with
+	  | Def lc1 ->
+	    let c1 = force_constr lc1 in
+            let c2 = force_constr lc2 in
+	    Reduction.conv env c1 c2
+	  (* Coq only places transparent cb in With_definition_body *)
+	  | _ -> assert false)
+    | _ -> ()) (* Pierre L: shouldn't this case raise an error ? *)
 
 let lookup_modtype mp env =
   try Environ.lookup_modtype mp env
diff --git a/checker/modops.ml b/checker/modops.ml
index b18b58a9f..4e2bbc210 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -95,19 +95,14 @@ and add_module mb env =
 
 
 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 = Const con in 
-      let const_subs = Some (Declarations.from_val const) in
-	{cb with 
-	   const_body = const_subs;
-	   const_opaque = false;
-	}
-	  
+      (* let con =  constant_of_delta resolver con in*)
+      let const = Const con in
+      let def = Def (Declarations.from_val const) in
+      { cb with const_body = def }
 
 let rec strengthen_mod env mp_from mp_to mb = 
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index eaf2aae80..bc067dc5f 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -77,15 +77,18 @@ type compiled_library =
 module LightenLibrary : sig
   type table 
   type lightened_compiled_library 
-  val load : load_proof:bool -> (unit -> table) 
-    -> lightened_compiled_library -> compiled_library
+  val load : table -> 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_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 
@@ -115,8 +118,8 @@ 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 cb) when is_opaque cb ->
+	  SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
 	| (SFBconst _ | SFBmind _ ) as x -> 
 	  x
 	| SFBmodule m -> 
@@ -148,21 +151,16 @@ 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 (table.(
-	    try 
-	      match Declarations.force_constr cterm with
-		| Term.Rel key -> key
-		| _ -> assert false
-	    with _ -> assert false
-	  ))
-	  | _ -> None
-      else 
-	fun _ -> None
+  let load table lightened_library =
+    let decode_key = function
+      | Undef _ | Def _ -> assert false
+      | OpaqueDef k ->
+          let k = key_of_lazy_constr k in
+	  let body =
+	    try table.(k)
+	    with _ -> error "Error while retrieving an opaque body"
+	  in
+	  OpaqueDef (lazy_constr_from_val body)
     in
     traverse_library decode_key lightened_library
 
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 986393b29..cd2c06d20 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -33,12 +33,8 @@ sig
   type table 
   type lightened_compiled_library 
 
-  (** [load lpf get_table lcl] builds a compiled library from a
+  (** [load table lcl] builds a compiled library from a
       lightened library [lcl] by remplacing every index by its related
-      opaque terms inside the table obtained by [get_table ()].  
-      If [lpf] is unset then the table is considered empty, which 
-      implies that [get_table] is not evaluated and every index 
-      is replaced by [None] inside the compiled library. *)
-  val load : load_proof:bool -> (unit -> table) 
-    -> lightened_compiled_library -> compiled_library
+      opaque terms inside [table]. *)
+  val load : table -> lightened_compiled_library -> compiled_library
 end
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 670f2783b..e00671b03 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -237,22 +237,26 @@ let check_constant 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
-	  let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-	  let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-	    check_type env typ1 typ2;
-	  let con = make_con mp1 empty_dirpath l in
-	    (match cb2 with
-               | {const_body=Some lc2;const_opaque=false} ->
-		   let c2 = force_constr lc2 in
-		   let c1 = match cb1.const_body with
-		     | Some lc1 -> force_constr lc1
-		     | None -> Const con
-		   in
-		     check_conv conv env c1 c2
-               | _ -> ())
+	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
+	check_type env typ1 typ2;
+	(* Now we check the bodies *)
+	(match cb2.const_body with
+	  | Undef _ -> ()
+	  | 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 ()
+	      | Def lc1 ->
+		let c1 = force_constr lc1 in
+		let c2 = force_constr lc2 in
+		check_conv conv env c1 c2)
+	  | OpaqueDef lc2 -> ()) (* Pierre L. : this looks really strange ?! *)
       | IndType ((kn,i),mind1) ->
 	  ignore (Util.error (
 		    "The kernel does not recognize yet that a parameter can be " ^
@@ -260,7 +264,7 @@ let check_constant 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 () ;
+      if constant_has_body cb2 then error () ;
       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 conv_leq env arity1 typ2
@@ -271,7 +275,7 @@ let check_constant 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 () ;
+      if constant_has_body cb2 then error () ;
       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 conv env ty1 ty2
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 337b90751..bd12528c7 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 403c1c7b5..74fb3f7ff 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 87474b863..02330339d 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 4b8b4537c..5f31ff8ce 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 fc8064d59..f092c8261 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 d4c86fb35..ebedd17e6 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 34074b677..a69a98c1b 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 f26d49dde..af1e17591 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 335c2a94e..aad541d21 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 6d4ebb989..df9b7e81f 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 8f4ec76f8..bdffa6802 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 0ab70b69e..3a7954874 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 0c7299508..cac55f4be 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 801bd6c80..8146ea7c1 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 8b48fc3cf..158f2c787 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
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 6d1fb7fae..547e394aa 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -29,7 +29,9 @@ let term_quality = ref false
 
 let xml_export = ref false
 
-let load_proofs = ref true
+type load_proofs = Force | Lazy | Dont
+
+let load_proofs = ref Lazy
 
 let raw_print = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 20e3a7819..dd0f33ae4 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -21,7 +21,8 @@ val term_quality : bool ref
 
 val xml_export : bool ref
 
-val load_proofs : bool ref
+type load_proofs = Force | Lazy | Dont
+val load_proofs : load_proofs ref
 
 val raw_print : bool ref
 
diff --git a/library/impargs.ml b/library/impargs.ml
index fad81b152..3f60bf96a 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -157,7 +157,7 @@ let is_flexible_reference env bound depth f =
     | Rel n -> (* since local definitions have been expanded *) false
     | Const kn ->
         let cb = Environ.lookup_constant kn env in
-        cb.const_body <> None & not cb.const_opaque
+	(match cb.const_body with Def _ -> true | _ -> false)
     | Var id ->
         let (_,value,_) = Environ.lookup_named id env in value <> None
     | Ind _ | Construct _ -> false
diff --git a/library/library.ml b/library/library.ml
index 3d72c5fdb..447d53610 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -382,25 +382,39 @@ let try_locate_qualified_library (loc,qid) =
 (************************************************************************)
 (* Internalise libraries *)
 
-let mk_library md get_table digest = 
-  let md_compiled = 
-    LightenLibrary.load ~load_proof:!Flags.load_proofs get_table md.md_compiled
+let mk_library md table digest =
+  let md_compiled =
+    LightenLibrary.load ~load_proof:!Flags.load_proofs table md.md_compiled
   in {
     library_name     = md.md_name;
     library_compiled = md_compiled;
     library_objects  = md.md_objects;
     library_deps     = md.md_deps;
     library_imports  = md.md_imports;
-    library_digest    = digest 
+    library_digest    = digest
   }
 
+let fetch_opaque_table (f,pos,digest) =
+  try
+    let ch = System.with_magic_number_check raw_intern_library f in
+    seek_in ch pos;
+    if System.marshal_in ch <> digest then failwith "File changed!";
+    let table = (System.marshal_in ch : LightenLibrary.table) in
+    close_in ch;
+    table
+  with _ ->
+    error
+      ("The file "^f^" is inaccessible or has changed,\n" ^
+       "cannot load some opaque constant bodies in it.\n")
+
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
   let lmd = System.marshal_in ch in
+  let pos = pos_in ch in
   let digest = System.marshal_in ch in
-  let get_table () = (System.marshal_in ch : LightenLibrary.table) in
+  let table = lazy (fetch_opaque_table (f,pos,digest)) in
   register_library_filename lmd.md_name f;
-  let library = mk_library lmd get_table digest in
+  let library = mk_library lmd table digest in
   close_in ch;
   library
 
diff --git a/library/states.ml b/library/states.ml
index 4619b3b53..c88858f7e 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -20,7 +20,10 @@ let unfreeze (fl,fs) =
 let (extern_state,intern_state) =
   let (raw_extern, raw_intern) =
     extern_intern Coq_config.state_magic_number ".coq" in
-  (fun s -> raw_extern s (freeze())),
+  (fun s ->
+    if !Flags.load_proofs <> Flags.Force then
+      Util.error "Write State only works with option -force-load-proofs";
+    raw_extern s (freeze())),
   (fun s ->
     unfreeze
       (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 3b979f519..17feae4ed 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -163,10 +163,11 @@ let opacity env = function
       Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v)))
   | ConstRef cst ->
       let cb = Environ.lookup_constant cst env in
-      if cb.const_body = None then None
-      else if cb.const_opaque then Some FullyOpaque
-      else Some
-        (TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst)))
+      (match cb.const_body with
+	| Undef _ -> None
+	| OpaqueDef _ -> Some FullyOpaque
+	| Def _ -> Some
+          (TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst))))
   | _ -> None
 
 let print_opacity ref =
@@ -439,7 +440,7 @@ let ungeneralized_type_of_constant_type = function
 
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
-  let val_0 = cb.const_body in
+  let val_0 = body_of_constant cb in
   let typ = ungeneralized_type_of_constant_type cb.const_type in
   hov 0 (
     match val_0 with
@@ -586,22 +587,21 @@ let print_full_pure_context () =
       | "CONSTANT" ->
 	  let con = Global.constant_of_delta (constant_of_kn kn) in
 	  let cb = Global.lookup_constant con in
-	  let val_0 = cb.const_body in
 	  let typ = ungeneralized_type_of_constant_type cb.const_type in
 	  hov 0 (
-	    match val_0 with
-	    | None ->
-		str (if cb.const_opaque then "Axiom " else "Parameter ") ++
+	    match cb.const_body with
+	      | Undef _ ->
+		str "Parameter " ++
 		print_basename con ++ str " : " ++ cut () ++ pr_ltype typ
-	    | Some v ->
-		if cb.const_opaque then
-		  str "Theorem " ++ print_basename con ++ cut () ++
-		  str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
-		  str "Proof " ++ print_body val_0
-		else
-		  str "Definition " ++ print_basename con ++ cut () ++
-		  str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
-		  print_body val_0) ++ str "." ++ fnl () ++ fnl ()
+	      | OpaqueDef lc ->
+		str "Theorem " ++ print_basename con ++ cut () ++
+		str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
+		str "Proof " ++ pr_lconstr (Declarations.force_opaque lc)
+	      | Def c ->
+		str "Definition " ++ print_basename con ++ cut () ++
+		str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
+		pr_lconstr (Declarations.force c))
+          ++ str "." ++ fnl () ++ fnl ()
       | "INDUCTIVE" ->
 	  let mind = Global.mind_of_delta (mind_of_kn kn) in
 	  let (mib,mip) = Global.lookup_inductive (mind,0) in
@@ -686,7 +686,7 @@ let print_opaque_name qid =
   match global qid with
     | ConstRef cst ->
 	let cb = Global.lookup_constant cst in
-        if cb.const_body <> None then
+        if constant_has_body cb then
 	  print_constant_with_infos cst
         else
 	  error "Not a defined constant."
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 16f6e6c9d..9440a61bf 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -97,24 +97,27 @@ and print_modtype locals mty =
 	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
 
 and print_sig locals sign = 
-  let print_spec (l,spec) = (match spec with
-    | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
-    | SFBconst {const_body=None}
-    | SFBconst {const_opaque=true} -> str "Parameter "
-    | SFBmind _ -> str "Inductive "
-    | SFBmodule _ -> str "Module "
-    | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
+  let print_spec (l,spec) = str (match spec with
+    | SFBconst cb ->
+      (match cb.const_body with
+	| Def _ -> "Definition "
+	| Undef _ | OpaqueDef _ -> "Parameter ")
+    | SFBmind _ -> "Inductive "
+    | SFBmodule _ -> "Module "
+    | SFBmodtype _ -> "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_spec sign
 
 and print_struct locals struc = 
-  let print_body (l,body) = (match body with
-    | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
-    | SFBconst {const_body=Some _; const_opaque=true} -> str "Theorem "
-    | SFBconst {const_body=None} -> str "Parameter "
-    | SFBmind _ -> str "Inductive "
-    | SFBmodule _ -> str "Module "
-    | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
+  let print_body (l,body) = str (match body with
+    | SFBconst cb ->
+      (match cb.const_body with
+	| Undef _ -> "Parameter "
+	| Def _ -> "Definition "
+	| OpaqueDef _ -> "Theorem ")
+    | SFBmind _ -> "Inductive "
+    | SFBmodule _ -> "Module "
+    | SFBmodtype _ -> "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_body struc
 
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 00a76efa3..b025cea64 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -468,7 +468,7 @@ and axiomatize_body env r id d = match r with
   | VarRef _ ->
       assert false
   | ConstRef c ->
-      begin match (Global.lookup_constant c).const_body with
+      begin match body_of_constant (Global.lookup_constant c) with
 	| Some b ->
 	    let b = force b in
 	    let axioms =
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 04d1f2a8d..c4dce1c7b 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -130,12 +130,12 @@ let check_arity env cb =
 
 let check_fix env cb i =
   match cb.const_body with
-    | None -> raise Impossible
-    | Some lbody ->
-	match kind_of_term (Declarations.force lbody) with
+    | Def lbody ->
+	(match kind_of_term (Declarations.force lbody) with
 	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
-	  | _ -> raise Impossible
+	  | _ -> raise Impossible)
+    | Undef _ | OpaqueDef _ -> raise Impossible
 
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 51d79e821..992f8fca6 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -245,7 +245,7 @@ let rec extract_type env db j c args =
 	(match flag_of_type env typ with
 	   | (Info, TypeScheme) ->
 	       let mlt = extract_type_app env db (r, type_sign env typ) args in
-	       (match cb.const_body with
+	       (match body_of_constant cb with
 		  | None -> mlt
 		  | Some _ when is_custom r -> mlt
 		  | Some lbody ->
@@ -258,7 +258,7 @@ let rec extract_type env db j c args =
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
 		      if expand env mlt = expand env mlt' then mlt else mlt')
 	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
-	       (match cb.const_body with
+	       (match body_of_constant cb with
 		  | None -> Tunknown (* Brutal approximation ... *)
 		  | Some lbody ->
 		      (* We try to reduce. *)
@@ -478,7 +478,7 @@ and mlt_env env r = match r with
        with Not_found ->
 	 let cb = Environ.lookup_constant kn env in
 	 let typ = Typeops.type_of_constant_type env cb.const_type in
-	 match cb.const_body with
+	 match body_of_constant cb with
 	   | None -> None
 	   | Some l_body ->
 	       (match flag_of_type env typ with
@@ -904,15 +904,9 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 let extract_constant env kn cb =
   let r = ConstRef kn in
   let typ = Typeops.type_of_constant_type env cb.const_type in
-  let warn_info_none () =
-    if not (is_custom r) then begin
-      add_info_axiom r;
-      if not !Flags.load_proofs && cb.const_opaque then add_opaque_ko r
-    end
-  in
-  let warn_info_some () = if cb.const_opaque then add_opaque_ok r
-  in
-  match cb.const_body with
+  let warn_info_none () = if not (is_custom r) then add_info_axiom r in
+  let warn_info_some () = if is_opaque cb then add_opaque r in
+  match body_of_constant cb with
     | None ->
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) ->
@@ -951,7 +945,7 @@ let extract_constant_spec env kn cb =
     | (Logic, Default) -> Sval (r, Tdummy Kother)
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
-	(match cb.const_body with
+	(match body_of_constant cb with
 	  | None -> Stype (r, vl, None)
 	  | Some body ->
 	      let db = db_from_sign s in
@@ -966,7 +960,7 @@ let extract_with_type env cb =
   match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
-	let body = Option.get cb.const_body in
+	let body = Option.get (body_of_constant cb) in
 	let db = db_from_sign s in
 	let t = extract_type_scheme env db (force body) (List.length s) in
 	Some (vl, t)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 3036cb134..4ab7b6f75 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1205,12 +1205,14 @@ let inline_test r t =
   if not (auto_inline ()) then false
   else
     let c = match r with ConstRef c -> c | _ -> assert false in
-    let body = try (Global.lookup_constant c).const_body with _ -> None in
-    if body = None then false
-    else
-      let t1 = eta_red t in
-      let t2 = snd (collect_lams t1) in
-      not (is_fix t2) && ml_size t < 12 && is_not_strict t
+    let has_body =
+      try constant_has_body (Global.lookup_constant c)
+      with _ -> false
+    in
+    has_body &&
+      (let t1 = eta_red t in
+       let t2 = snd (collect_lams t1) in
+       not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
   let null = empty_dirpath in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 8c9fdf37d..35494d3d2 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -175,14 +175,10 @@ let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
 let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
 let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
-let opaques_ok = ref Refset'.empty
-let opaques_ko = ref Refset'.empty
-let init_opaques () = opaques_ok := Refset'.empty; opaques_ko := Refset'.empty
-let add_opaque_ok r = opaques_ok := Refset'.add r !opaques_ok
-let add_opaque_ko r = opaques_ko := Refset'.add r !opaques_ko
-let remove_opaque r =
-  opaques_ok := Refset'.remove r !opaques_ok;
-  opaques_ko := Refset'.remove r !opaques_ko
+let opaques = ref Refset'.empty
+let init_opaques () = opaques := Refset'.empty
+let add_opaque r = opaques := Refset'.add r !opaques
+let remove_opaque r = opaques := Refset'.remove r !opaques
 
 (*s Extraction modes: modular or monolithic, library or minimal ?
 
@@ -263,23 +259,19 @@ let warning_axioms () =
        str "Having invalid logical axiom in the environment when extracting" ++
        spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
        fnl ())
-  end
+  end;
+  if !Flags.load_proofs = Flags.Dont && info_axioms@log_axioms <> [] then
+    msg_warning
+      (str "Some of these axioms might by due to option -dont-load-proofs.")
 
 let warning_opaques () =
-  let opaques_ok = Refset'.elements !opaques_ok in
-  if opaques_ok = [] then ()
+  let opaques = Refset'.elements !opaques in
+  if opaques = [] then ()
   else msg_warning
     (str "Extraction is accessing the body of the following opaque constants:"
-     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques_ok)
+     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques)
      ++ str "." ++ fnl ()
-     ++ str "Be careful if using option -dont-load-proofs later." ++ fnl ());
-  let opaques_ko = Refset'.elements !opaques_ko in
-  if opaques_ko = [] then ()
-  else msg_warning
-    (str "Extraction cannot access the body of the following opaque constants:"
-     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques_ko)
-     ++ fnl () ++ str "due to option -dont-load-proofs. "
-     ++ str "These constants are treated as axioms." ++ fnl ())
+     ++ str "Be careful if using option -dont-load-proofs later." ++ fnl ())
 
 let warning_both_mod_and_cst q mp r =
  msg_warning
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 158e33ec9..97c28b154 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -84,8 +84,7 @@ val add_info_axiom : global_reference -> unit
 val remove_info_axiom : global_reference -> unit
 val add_log_axiom : global_reference -> unit
 
-val add_opaque_ok : global_reference -> unit
-val add_opaque_ko : global_reference -> unit
+val add_opaque : global_reference -> unit
 val remove_opaque : global_reference -> unit
 
 val reset_tables : unit -> unit
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2c5118e92..4f32bbd99 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -935,7 +935,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let f_def = Global.lookup_constant (destConst f) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body =
-    force (Option.get f_def.const_body)
+    force (Option.get (body_of_constant f_def))
   in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -1051,7 +1051,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
       }
     in
     let get_body const =
-      match (Global.lookup_constant const ).const_body with
+      match body_of_constant (Global.lookup_constant const) with
 	| Some b ->
 	     let body = force b in
 	     Tacred.cbv_norm_flags
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1d089409b..2ba29ced7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -445,7 +445,7 @@ let get_funs_constant mp dp =
   in
   function const ->
     let find_constant_body const =
-      match (Global.lookup_constant const ).const_body with
+      match body_of_constant (Global.lookup_constant const) with
 	| Some b ->
 	    let body = force b in
 	    let body = Tacred.cbv_norm_flags
@@ -579,7 +579,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition
     let finfos = find_Function_infos this_block_funs.(0) in
     try
       let equation =  Option.get finfos.equation_lemma in
-      (Global.lookup_constant equation).Declarations.const_opaque
+      Declarations.is_opaque (Global.lookup_constant equation)
     with Option.IsNone -> (* non recursive definition *)
       false
   in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 38492f88b..dd48765fb 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -834,7 +834,7 @@ let make_graph (f_ref:global_reference) =
       | _ -> raise (UserError ("", str "Not a function reference") )
   in
   Dumpglob.pause ();
-  (match c_body.const_body with
+  (match body_of_constant c_body with
      | None -> error "Cannot build a graph over an axiom !"
      | Some b ->
 	 let env = Global.env () in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 1de0f91d1..094d2e50f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -120,9 +120,9 @@ let const_of_id id =
 let def_of_const t =
    match (Term.kind_of_term t) with
     Term.Const sp ->
-      (try (match (Global.lookup_constant sp) with
-             {Declarations.const_body=Some c} -> Declarations.force c
-	     |_ -> assert false)
+      (try (match Declarations.body_of_constant (Global.lookup_constant sp) with
+             | Some c -> Declarations.force c
+	     | _ -> assert false)
        with _ -> assert false)
     |_ -> assert false
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4217b83fa..11fbc01ba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -136,9 +136,9 @@ let message s = if Flags.is_verbose () then msgnl(str s);;
 let def_of_const t =
    match (kind_of_term t) with
     Const sp ->
-      (try (match (Global.lookup_constant sp) with
-             {const_body=Some c} -> Declarations.force c
-	     |_ -> assert false)
+      (try (match body_of_constant (Global.lookup_constant sp) with
+             | Some c -> Declarations.force c
+	     | _ -> assert false)
        with _ ->
 	 anomaly ("Cannot find definition of constant "^
 		    (string_of_id (id_of_label (con_label sp))))
@@ -939,6 +939,13 @@ let build_new_goal_type () =
   let res = build_and_l sub_gls_types in
   res
 
+let is_opaque_constant c =
+  let cb = Global.lookup_constant c in
+  match cb.Declarations.const_body with
+    | Declarations.OpaqueDef _ -> true
+    | Declarations.Undef _ -> true
+    | Declarations.Def _ -> false
+
 let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
   let current_proof_name = get_current_proof_name () in
@@ -958,10 +965,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
       let na_ref = Libnames.Ident (dummy_loc,na) in
       let na_global = Nametab.global na_ref in
       match na_global with
-	  ConstRef c ->
-	    let cb = Global.lookup_constant c in
-	    if cb.Declarations.const_opaque then true
-	    else begin  match cb.const_body with None -> true | _ -> false end
+	  ConstRef c -> is_opaque_constant c
 	| _ -> anomaly "equation_lemma: not a constant"
     in
     let lemma = mkConst (Lib.make_con na) in
@@ -1339,10 +1343,7 @@ let (com_eqn : int -> identifier ->
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
     let opacity =
       match terminate_ref with
-	| ConstRef c ->
-	    let cb = Global.lookup_constant c in
-	    if cb.Declarations.const_opaque then true
-	    else begin match cb.const_body with None -> true | _ -> false end
+	| ConstRef c -> is_opaque_constant c
 	| _ -> anomaly "terminate_lemma: not a constant"
     in
     let (evmap, env) = Lemmas.get_current_context() in
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index f0a5089cc..78048c8ee 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -527,8 +527,10 @@ let print internal glob_ref kind xml_library_root =
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Ln.ConstRef kn ->
        let id = N.id_of_label (N.con_label kn) in
-       let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
-        G.lookup_constant kn in
+       let cb = G.lookup_constant kn in
+       let val0 = D.body_of_constant cb in
+       let typ = cb.D.const_type in
+       let hyps = cb.D.const_hyps in
        let typ = Typeops.type_of_constant_type (Global.env()) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 69ef4598d..c6b3339d7 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -38,12 +38,13 @@ let set_strategy_one ref l  =
         Csymtable.set_opaque_const sp
     | ConstKey sp, _ ->
         let cb = Global.lookup_constant sp in
-        if cb.const_body <> None & cb.const_opaque then
-          errorlabstrm "set_transparent_const"
-            (str "Cannot make" ++ spc () ++
-            Nametab.pr_global_env Idset.empty (ConstRef sp) ++
-            spc () ++ str "transparent because it was declared opaque.");
-        Csymtable.set_transparent_const sp
+	(match cb.const_body with
+	  | OpaqueDef _ ->
+            errorlabstrm "set_transparent_const"
+              (str "Cannot make" ++ spc () ++
+		 Nametab.pr_global_env Idset.empty (ConstRef sp) ++
+		 spc () ++ str "transparent because it was declared opaque.");
+	  | _ -> Csymtable.set_transparent_const sp)
     | _ -> ()
 
 let cache_strategy (_,str) =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 93476f4c4..e0f21aab8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -189,7 +189,8 @@ let parse_args arglist =
     | "-batch" :: rem -> set_batch_mode (); parse rem
     | "-boot" :: rem -> boot := true; no_load_rc (); parse rem
     | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem
-    | "-outputstate" :: s :: rem -> set_outputstate s; parse rem
+    | "-outputstate" :: s :: rem ->
+      Flags.load_proofs := Flags.Force; set_outputstate s; parse rem
     | "-outputstate" :: []       -> usage ()
 
     | "-nois" :: rem -> set_inputstate ""; parse rem
@@ -230,8 +231,9 @@ let parse_args arglist =
     | "-compile-verbose" :: f :: rem -> add_compile true f;  if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
     | "-compile-verbose" :: []       -> usage ()
 
-    | "-load-proofs" :: rem -> Flags.load_proofs := true; parse rem
-    | "-dont-load-proofs" :: rem -> Flags.load_proofs := false; parse rem
+    | "-force-load-proofs" :: rem -> Flags.load_proofs := Flags.Force; parse rem
+    | "-lazy-load-proofs" :: rem -> Flags.load_proofs := Flags.Lazy; parse rem
+    | "-dont-load-proofs" :: rem -> Flags.load_proofs := Flags.Dont; parse rem
 
     | "-beautify" :: rem -> make_beautify true; parse rem
 
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 2d904c554..7cc9ba33e 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -39,8 +39,8 @@ let retrieve_first_recthm = function
   | VarRef id ->
       (pi2 (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
-      let {const_body=body;const_opaque=opaq} =	Global.lookup_constant cst in
-      (Option.map Declarations.force body,opaq)
+      let cb = Global.lookup_constant cst in
+      (Option.map Declarations.force (body_of_constant cb), is_opaque cb)
   | _ -> assert false
 
 let adjust_guardness_conditions const = function
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 84e38c0a1..e09706325 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -61,8 +61,10 @@ let print_usage_channel co command =
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
 \n  -impredicative-set     set sort Set impredicative\
-\n  -load-proofs           load opaque proofs in memory (default)\
-\n  -dont-load-proofs      don't load opaque proofs in memory\
+\n  -force-load-proofs     load opaque proofs in memory initially\
+
+\n  -lazy-load-proofs      load opaque proofs in memory by necessity (default)\
+\n  -dont-load-proofs      see opaque proofs as axioms instead of loading them\
 \n  -xml                   export XML files either to the hierarchy rooted in\
 \n                         the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
 \n                         stdout (if unset)\