summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /library
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'library')
-rw-r--r--library/dischargedhypsmap.ml4
-rw-r--r--library/library.ml4
2 files changed, 4 insertions, 4 deletions
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 255f5e75..f515dcb0 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dischargedhypsmap.ml 9488 2007-01-17 11:11:58Z herbelin $ *)
+(* $Id: dischargedhypsmap.ml 9903 2007-06-21 17:02:07Z herbelin $ *)
open Util
open Libnames
@@ -31,7 +31,7 @@ let get_discharged_hyps sp =
try
Spmap.find sp !discharged_hyps_map
with Not_found ->
- anomaly ("No discharged hypothesis for object " ^ string_of_path sp)
+ []
(*s Registration as global tables and rollback. *)
diff --git a/library/library.ml b/library/library.ml
index b68c3eb5..3a3328ad 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml 9637 2007-02-10 08:32:28Z notin $ *)
+(* $Id: library.ml 9525 2007-01-24 08:43:01Z herbelin $ *)
open Pp
open Util
@@ -300,7 +300,7 @@ let (in_import, out_import) =
(*s Loading from disk to cache (preparation phase) *)
-let vo_magic_number = 080100 (* V8.1 *)
+let vo_magic_number = 080992 (* V8.1 beta2 *)
let (raw_extern_library, raw_intern_library) =
System.raw_extern_intern vo_magic_number ".vo"