* checker/Safe_typing.LightenLibrary:

  Remove the function "save" as the checker only needs to read vo files.

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

2 files changed, 0 insertions, 36 deletions

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 39904df8d..70eccf952 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -79,7 +79,6 @@ type compiled_library =
 module LightenLibrary : sig
   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
 end = struct
@@ -132,37 +131,6 @@ end = struct
     in
     fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s) 
 
-  (* To disburden a library from opaque definitions, we simply 
-     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), 
-	 (get_table : unit -> table)) = 
-      (* We use an integer as a key inside the table. *)
-      let counter = ref 0 in
-      (* ... but it is wrapped inside a [constr_substituted]. *)
-      let key_as_constr key = Declarations.from_val (Term.Rel 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), 
-
-       (* 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
-    (lightened_library, get_table ())
-
   (* Loading is also a traversing that decodes the embedded keys that
      are inside the [lightened_library]. If the [load_proof] flag is
      set, we lookup inside the table to graft the
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 78107455c..73f705182 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -34,10 +34,6 @@ sig
   type table 
   type lightened_compiled_library 
 
-  (** [save] splits a library into a lightened library with indexes
-      and a table that maps these indexes to opaque terms. *)
-  val save : compiled_library -> lightened_compiled_library * table
-
   (** [load lpf get_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 ()].