new csdp cache + improved error message

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

1 files changed, 4 insertions, 12 deletions

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index cbacc48e4..87c9d1bbe 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -25,7 +25,9 @@ module type PHashtable =
 
 
     val open_in : string -> 'a t
-    (** [open_in f] rebuilds a table from the records stored in file [f] *)
+    (** [open_in f] rebuilds a table from the records stored in file [f].
+	As marshaling is not type-safe, it migth segault.
+    *)
 
     val find : 'a t -> key -> 'a
     (** find has the specification of Hashtable.find *)
@@ -42,7 +44,7 @@ module type PHashtable =
 
     val memo : string -> (key -> 'a) -> (key -> 'a)
       (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
-	  Note that the cache is just loaded when needed *)
+	  Note that the cache will only be loaded when the function is used for the first time *)
 
   end
 
@@ -89,16 +91,6 @@ let finally f rst =
     ); raise x
 
 
-(** [from_file f] returns a hashtable by parsing records from file [f].
-    Elements of the file are marshelled pairs of Caml structures.
-    (To ensure portability across platforms, closures are not allowed.)
-
-    Raises Sys_error if the file cannot be open
-    Raises InvalidTableFormat if the file does not conform to the format
-    i.e, Marshal.from_channel fails
-*)
-
-
 let read_key_elem inch =
   try
     Some (Marshal.from_channel inch)