From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 library/dischargedhypsmap.ml | 16 ++--------------
 1 file changed, 2 insertions(+), 14 deletions(-)

(limited to 'library/dischargedhypsmap.ml')

diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 2a3abda8..255f5e75 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dischargedhypsmap.ml 6748 2005-02-18 22:17:50Z herbelin $ *)
+(* $Id: dischargedhypsmap.ml 9488 2007-01-17 11:11:58Z herbelin $ *)
 
 open Util
 open Libnames
@@ -24,21 +24,9 @@ type discharged_hyps = section_path list
 
 let discharged_hyps_map = ref Spmap.empty
 
-let load_discharged_hyps_map _ (_,(sp,hyps)) = 
+let set_discharged_hyps sp hyps = 
   discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
 
-let cache_discharged_hyps_map o =
-  load_discharged_hyps_map 1 o
-
-let (in_discharged_hyps_map, _) =
-  declare_object { (default_object "DISCHARGED-HYPS-MAP") with
-    cache_function = cache_discharged_hyps_map;
-    load_function = load_discharged_hyps_map;
-    export_function = (fun x -> Some x) }
-
-let set_discharged_hyps sp hyps =
- add_anonymous_leaf (in_discharged_hyps_map (sp,hyps))
-
 let get_discharged_hyps sp =
   try
    Spmap.find sp !discharged_hyps_map
-- 
cgit v1.2.3